lean4

lean4 copied to clipboard

RFC: new versus old code generator issue

16

Since `nightly-2025-06-21` the file `CoreM.lean` changed line `670` to `defValue := true`. The new code generator does not want to generate code any more for the some of my code....

LucDuponcheelAtGitHub

Errors in `do`-notation pattern variables swallowed by "unsupported syntax pattern"

1

### Description Ambiguous name errors while pattern matching in `do`-notation are swallowed and replaced by an unrelated message about syntax pattern matching. ### Context This occurred while migrating Verso code...

david-christiansen

Consider ``` -- import Lean set_option linter.unusedSimpArgs false example : True := by simp [BitVec.reduceEq] ``` hovering over the simproc it just says ``` A simp lemma specification is: optional...

nomeata

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

JovanGerb

split fails with non-fvar discriminants and dependent motives

2

Consider this ``` /-- error: Tactic `split` failed: Could not split an `if` or `match` expression in the goal n : Nat ⊢ Fin.last n = match id n with...

nomeata

Cannot derive functional induction principle: failed to transform matcher, type error when constructing new pre-splitter motive

3

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

TwoFX

### Proposal We should support attribute declaration modifiers on inductive constructors. This would allow the following example from mathlib [here](https://github.com/leanprover-community/mathlib4/blob/f0e5f810b831671addae1078f6e05fb3697276ab/Mathlib/Logic/Relation.lean#L256-L262): ```lean @[mk_iff ReflTransGen.cases_tail_iff] inductive ReflTransGen (r : α → α...

mtoohey31

RFC: guard patterns

4

This is split out of #371. I would like to see support for match guards: some sort of boolean clause attached to a match branch which must return true if...

omentic

`simp`, `omega` in `module` cause type mismatch in kernel

2

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

datokrat

`simp` unable to rewrite seemingly identical terms

2

### Prerequisites Please put an X between the brackets as you perform the following steps: * [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [X] Reduce the...

zhengyao-lin