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

fix: missing condition

Browse source
This commit is contained in:
Leonardo de Moura 2021-07-21 07:36:35 -07:00
parent c5ffcc5dd6
commit a6af257b7a
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/Contradiction.lean
View file

@ -62,7 +62,7 @@ def contradictionCore (mvarId : MVarId) (useDecide : Bool) (searchDepth : Nat) :
assignExprMVar mvarId (← mkNoConfusion (← getMVarType mvarId) localDecl.toExpr)
return true
-- (h : p) s.t. `decide p` evaluates to `false`
if useDecide && !localDecl.type.hasFVar then
if useDecide && !localDecl.type.hasFVar && !localDecl.type.hasMVar then
try
let d ← mkDecide localDecl.type
let r ← withDefault <| whnf d