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

fix: typo

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-08 11:31:05 -07:00
parent c972742494
commit 74908bb9c7
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/Init/Lean/Meta/Tactic/Injection.lean
View file

@ -54,7 +54,7 @@ withMVarContext mvarId $ do
newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag;
assignExprMVar mvarId (mkApp val newMVar);
mvarId ← tryClear newMVar.mvarId! fvarId;
pure $ InjectionResultCore.subgoal newMVar.mvarId! aCtor.nfields
pure $ InjectionResultCore.subgoal mvarId aCtor.nfields
| _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction"
| _, _ => throwTacticEx `injection mvarId "equality of constructor applications expected"