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

chore: minor

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-21 20:53:19 -08:00
parent 8598dde6e6
commit e8ae23b7a6
2 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -905,9 +905,8 @@ 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 env ← getEnv
let tProj? := env.isProjectionFn tInfo.name
let sProj? := env.isProjectionFn sInfo.name
let tProj? ← isProjectionFn tInfo.name
let sProj? ← isProjectionFn sInfo.name
if tProj? && !sProj? then
unfold s (unfoldDefEq tInfo sInfo t s) $ fun s => isDefEqRight sInfo.name t s
else if !tProj? && sProj? then

7
src/Lean/ProjFns.lean
View file

@ -62,4 +62,11 @@ def getProjectionStructureName? (env : Environment) (projName : Name) : Option N
| _ => none
end Environment
def isProjectionFn [MonadEnv m] [Monad m] (declName : Name) : m Bool :=
return (← getEnv).isProjectionFn declName
def getProjectionFnInfo? [MonadEnv m] [Monad m] (declName : Name) : m (Option ProjectionFunctionInfo) :=
return (← getEnv).getProjectionFnInfo? declName
end Lean