Mario Carneiro

icon indicating a website link https://digama0.github.io/ icon indicating an email [email protected]

icon company Chalmers University of Technology icon location Gothenburg, Sweden icon location I'm a post-doc working on formal mathematics and interactive theorem proving. I am an expert in the Metamath and Lean proof languages.

Results 455 comments of Mario Carneiro

`interval_cases` for `pnat`s does not work, because `norm_num` does not support `pnat` (except sometimes)

We can't even use `prove_nat_uncast` in order to reflect it to a `nat` equality because this requires `semiring pnat`.

`rintro` error message is in the wrong place

The error should be on the `h`.

Rust-to-MiniRust translation can blow up exponentially

> Add support for memoization to specr, so that on Coq we can make it a NOP but in the translation to Rust we can have a global cache. I'm...

feat: notation for Euclidean space

My guess is that one of the linters is elaborating something in an empty environment, and it's failing to interpret the syntax objects. See [`6ed0fa63`](https://github.com/leanprover-community/batteries/commit/6ed0fa636779101a5619955b804d4786445d7e38) which was about a similar...

Rename buildheap executable

I don't see the advantage of `hol.bare` over `hol --bare`