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

fix: nat literals are constructor applications

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-08 17:44:53 -07:00
parent 21353d07d5
commit 7cf53b649b
1 changed files with 13 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Init/Lean/Meta/Tactic/Injection.lean
View file

@ -16,14 +16,20 @@ inductive InjectionResultCore
| solved
| subgoal (mvarId : MVarId) (numNewEqs : Nat)
def constructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
let f := e.getAppFn;
let nargs := e.getAppNumArgs;
private def getConstructorVal (ctorName : Name) (numArgs : Nat) : MetaM (Option ConstructorVal) := do
env ← getEnv;
matchConst env f (fun _ => pure none) $ fun cinfo _ =>
match cinfo with
| ConstantInfo.ctorInfo v => if e.getAppNumArgs == v.nparams + v.nfields then pure (some v) else pure none
| _ => pure none
match env.find? ctorName with
| some (ConstantInfo.ctorInfo v) => if numArgs == v.nparams + v.nfields then pure (some v) else pure none
| _ => pure none
def constructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
match e with
| Expr.lit (Literal.natVal n) _ =>
if n == 0 then getConstructorVal `Nat.zero 0 else getConstructorVal `Nat.succ 1
| _ =>
match e.getAppFn with
| Expr.const n _ _ => getConstructorVal n e.getAppNumArgs
| _ => pure none
def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCore := do
withMVarContext mvarId $ do