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

fix: missing HEq support at ToLCNF (#6311)

Browse source 
This PR adds support for `HEq` to the new code generator.
This commit is contained in:
Leonardo de Moura 2024-12-04 20:49:16 +01:00 • committed by GitHub
parent 88573c802d
commit f6e88e5a05
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Compiler/LCNF/ToLCNF.lean
View file

@ -593,6 +593,14 @@ where
let minor ← visit minor
mkOverApplication minor args arity
visitHEqRec (e : Expr) : M Arg :=
let arity := 7
etaIfUnderApplied e arity do
let args := e.getAppArgs
let minor := if e.isAppOf ``HEq.rec || e.isAppOf ``HEq.ndrec then args[3]! else args[6]!
let minor ← visit minor
mkOverApplication minor args arity
visitFalseRec (e : Expr) : M Arg :=
let arity := 2
etaIfUnderApplied e arity do
@ -669,6 +677,8 @@ where
visitCtor 3 e
else if declName == ``Eq.casesOn || declName == ``Eq.rec || declName == ``Eq.ndrec then
visitEqRec e
else if declName == ``HEq.casesOn || declName == ``HEq.rec || declName == ``HEq.ndrec then
visitHEqRec e
else if declName == ``And.rec || declName == ``Iff.rec then
visitAndIffRecCore e (minorPos := 3)
else if declName == ``And.casesOn || declName == ``Iff.casesOn then