max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: registers eqns info before adding definition

Browse source 
Otherwise `[simp]` at definition will fail to generate equational theorems.
This commit is contained in:
Leonardo de Moura 2022-01-06 12:24:40 -08:00
parent 7acbbb4fbb
commit d8d7d63830
2 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/PreDefinition/Structural/Main.lean
View file

@ -84,10 +84,10 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
let preDefNonRec ← eraseRecAppSyntax preDefNonRec
let preDef ← eraseRecAppSyntax preDefs[0]
state.addMatchers.forM liftM
registerEqnsInfo preDef recArgPos
mapError (addNonRec preDefNonRec) (fun msg => m!"structural recursion failed, produced type incorrect term{indentD msg}")
addAndCompilePartialRec #[preDef]
addSmartUnfoldingDef preDef recArgPos
registerEqnsInfo preDef recArgPos
builtin_initialize
registerTraceClass `Elab.definition.structural

11
tests/lean/run/simpAtDefIssue.lean Normal file
View file

@ -0,0 +1,11 @@
@[simp] def g (x y : Nat) : Nat :=
match x, y with
| 0, 0 => 1
| 0, y => y
| x+1, 5 => 2 * g x 0
| x+1, y => 2 * g x y
#check g._eq_1
#check g._eq_2
#check g._eq_3
#check g._eq_4