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

fix: allow recursive occurrences in binder types at WF/PackDomain.lean

Browse source 
fixes #1171
This commit is contained in:
Leonardo de Moura 2022-05-27 11:23:51 -07:00
parent 3be437cad3
commit fbd8224b4d
2 changed files with 27 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/Lean/Elab/PreDefinition/WF/PackDomain.lean
View file

@ -131,14 +131,20 @@ where
visit (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr := do
checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do
match e with
| Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars (usedLetOnly := false) xs (← visit b)
| Expr.letE n t v b _ => withLetDecl n t (← visit v) fun x => do mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
| Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars (usedLetOnly := false) xs (← visit b)
| Expr.proj n i s .. => return mkProj n i (← visit s)
| Expr.mdata d b _ => return mkMData d (← visit b)
| Expr.app .. => visitApp e
| Expr.const .. => visitApp e
| e => return e,
| Expr.lam n d b c =>
withLocalDecl n c.binderInfo (← visit d) fun x => do
mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
| Expr.forallE n d b c =>
withLocalDecl n c.binderInfo (← visit d) fun x => do
mkForallFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
| Expr.letE n t v b c =>
withLetDecl n (← visit t) (← visit v) fun x => do
mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
| Expr.proj n i s .. => return mkProj n i (← visit s)
| Expr.mdata d b _ => return mkMData d (← visit b)
| Expr.app .. => visitApp e
| Expr.const .. => visitApp e
| e => return e,
visitApp (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr := e.withApp fun f args => do
let args ← args.mapM visit
if let some funIdx := isAppOfPreDef? f then

13
tests/lean/run/1171.lean Normal file
View file

@ -0,0 +1,13 @@
def Nat.hasDecEq: (a: Nat) → (b: Nat) → Decidable (Eq a b)
| 0, 0 => isTrue rfl
| n+1, 0
| 0, n+1 => isFalse Nat.noConfusion
| n+1, m+1 =>
match h:hasDecEq n m with -- it works without `h:`
| isTrue heq => isTrue (heq ▸ rfl)
| isFalse hne => isFalse (Nat.noConfusion · (λ heq => absurd heq hne))
termination_by _ a b => (a, b)
set_option pp.proofs true
#print Nat.hasDecEq
#print Nat.hasDecEq._unary