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

fix: isDeltaCandidate?

Browse source 
It should return `some ...` only if `ConstantInfo` has a value.
This commit is contained in:
Leonardo de Moura 2021-02-05 09:19:37 -08:00
parent 10a10b38d8
commit c17a1c382f
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -938,10 +938,13 @@ private def processAssignment' (mvarApp : Expr) (v : Expr) : MetaM Bool := do
else
return false
private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) :=
private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) := do
match t.getAppFn with
| Expr.const c _ _ => getConst? c
| _ => pure none
| Expr.const c _ _ =>
match (← getConst? c) with
| r@(some info) => if info.hasValue then return r else return none
| _ => return none
| _ => pure none
/-- Auxiliary method for isDefEqDelta -/
private def isListLevelDefEq (us vs : List Level) : MetaM LBool :=