lean4

lean4 copied to clipboard

Use `Bool.asProp` for coercions

4

Fixes #2043.

gebner

Make `Decidable` a subtype of `Bool`

9

This resolves the diamond between `Decidable` and `BEq`, which is starting to cause lots of headaches in mathlib.

gebner

This adds two features to `#eval` that I've wanted for a long time. - Interactive expressions and traces. - Doesn't refuse to evaluate terms that have missing `Repr`/etc. instances. `#eval...

gebner

This adds: * a module doc for `Lean.Elab.StructInst`, which gives an overview of how the code for structure instance elaboration works * docstrings for each definition in `Lean.Elab.StructInst` Note: I'm...

thorimur

chore: CI: enable emulated tests on Linux aarch64

1

gebner

chore: normalize naming convention in theorems

4

Now that the [naming convention](https://github.com/leanprover-community/mathlib4/wiki#naming-convention) has been tested in mathlib, I think it is safe to backport the changes to lean core and normalize any remaining inconsistencies in theorem names....

digama0

feat: `show` tactic (full version)

2

This implements the TODO in the `show` tactic: `show e` will first try to change the goal to `e`, and if that doesn't work it will try to change one...

digama0

refactor: termination arguments as Expr, not Syntax

1

Before, the termination argument as inferred by `GuessLex` was passed further on as `Syntax`, to be elaborated later in `WF.Rel`. This didn’t feel quite right anymore. In particular if we...

nomeata

fix: jump to correct definition when names overlap

1

Fixes #1170. This PR adds the module name to `RefIdent` in order to distinguish conflicting names from different files. This also fixes related issues in find-references or the call hierarchy...

mhuisi

feat: add option `tactic.customEliminators` to be able to turn off custom eliminators for `induction` and `cases`

1

This was suggested by Scott Morrison to be able to help projects adjust to `Nat` having built-in custom eliminators.

kmill