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

chore: naming convention

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-04 14:22:16 -07:00
parent 2f0b65fad3
commit 4501bdecb1
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Meta/ExprDefEq.lean
View file

@ -1257,11 +1257,11 @@ private def unfoldReducibeDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : Meta
Auxiliary method for isDefEqDelta -/
private def unfoldNonProjFnDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : MetaM LBool := do
let tProj? ← isProjectionFn tInfo.name
let sProj? ← isProjectionFn sInfo.name
if tProj? && !sProj? then
let tIsProj ← isProjectionFn tInfo.name
let sIsProj ← isProjectionFn sInfo.name
if tIsProj && !sIsProj then
unfold s (unfoldDefEq tInfo sInfo t s) fun s => isDefEqRight sInfo.name t s
else if !tProj? && sProj? then
else if !tIsProj && sIsProj then
unfold t (unfoldDefEq tInfo sInfo t s) fun t => isDefEqLeft tInfo.name t s
else
unfoldReducibeDefEq tInfo sInfo t s