Mario Carneiro
Mario Carneiro
```lean def foo {α} : Array α → Array α | #[a] => #[a] | as => as theorem foo_eq {α} (as : Array α) : foo as = as...
MML comes with a `abstr/` directory containing: * `abstr/foo.abs` for each article `foo` * `abstr/reftags` * `abstr/symbtags` It is a mystery how these files are generated, since the build script...
This tactic solves problems in intuitionistic propositional logic. It also produces nice proofs when doing so, so it is useful even for proving classical theorems (using the `itauto!` variant to...
As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/missing.20doc.20of.20.60.23check_failure.60/near/434466058), the `#help` command is out of date with respect to the parsers that can be obscuring the search for the "first token", used to power the...
This solves the issue where certain subexpressions are lacking syntax hovers because the hover text is not "builtin" - it only shows up if the `Parser` constant is imported in...
Inspired by https://github.com/leanprover/lean4/pull/3867#discussion_r1559543688 . After playing with this function a bit more, I was able to confirm that it's not really possible to implement it tail recursively in most monads...
The `PersistentEnvExtension` type required that the data stored in an .olean file for the extension was of type `Array α` for some `α`, even though it did not really take...
Split off from #2704, cc: @semorrison
(This was issue was discovered while debugging `lean4lean`.) The kernel is_def_eq function is almost commutative, so this makes little difference, but it has one non-commutative case: https://github.com/leanprover/lean4/blob/fb0d0245db9bcb9ff649794f57522c52cb80c993/stage0/src/kernel/type_checker.cpp#L1006-L1013 This handles defeq...
This adapts the code from the `inferProjType` function and the kernel projection typechecker so that the elaborator correctly reports errors when the projection would be rejected by the kernel. Fixes...