Mario Carneiro
Mario Carneiro
Currently the implementation of `ring` is incomplete and has no understanding of subtraction or negation: ```lean import Mathlib.Tactic.Ring example (a b : ℤ) : a - b = a +...
This generalizes the `on_goal` tactic to allow targeting multiple goals at once, and it focuses on each of them when calling the given tactic sequence, like `all_goals` but for a...
Back from the dead (https://github.com/leanprover/lean/pull/1628). @cipher1024 @EdAyers There were some worrisome review comments about ts_clone that I don't think I addressed before the PR was closed. I'll take another look...
For some reason structure fields are not elaborated the same as other definitions when using projection notation, even when all the binder types and attributes are the same: ```lean class...
```lean section foo -- invalid declaration, 'constant/axiom' cannot be used in sections constant foo : Type end foo ``` AFAICT this is a restriction without a reason. It would be...
```racket #lang racket (require redex) (define-language A (N ::= 0 1 2)) (define-metafunction A flip : N -> N [(flip 1) ()] [(flip ()) 1]) (term (flip 1)) ; flip:...
This fixes an issue with hovers inside user attributes caused by the fact that the info nodes generated by the user attribute are not nested correctly under the attribute itself,...
This implements a feature similar to the `#[track_caller]` attribute in Rust or the `[HasCallStack]` typeclass in GHC Haskell. * The panicking primitive `panicWithPosWithDecl` and `panicWithPos` are changed to `StackInfo.panic` which...