Mario Carneiro

As (truncating) conversion for BigInt?

5

I might be missing it, but I don't see a version of `Wrapping` or other such wrapping conversions for `BigInt`. Specifically, I would like to be able to convert `n:...

Fixes #222. New public API: * `gltf::import` module (debatable: it would also be possible to keep this private and re-export the other functions) * `gltf::import::import` and `gltf::import::import_slice`: These were already...

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues). *...

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues). *...

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues). *...

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues). *...

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues). *...

Can't refer to anonymous match in section with parameters

1

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues). *...

Mixing absolute and relative imports causes duplicate definition error

4

The test has directory structure `test/{a,b,c}.lean`. In each file: a.lean: inductive A b.lean: import test.a c.lean: import .b .a -- Error: invalid import: a -- invalid object declaration, environment already...

This makes the `foo` in `syntax (name := foo) ...` act like a declaration name for the purpose of hovers (so by hovering on it you can see the rendered...