feat: Prograde tactics #83
|
@ -62,7 +62,7 @@ def collectMotiveArguments (forallBody: Expr): SSet Nat :=
|
|||
| _ => SSet.empty
|
||||
|
||||
/-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
|
||||
def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (List Meta.InductionSubgoal) := mvarId.withContext do
|
||||
def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.InductionSubgoal) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
|
||||
let recursorType ← Meta.inferType recursor
|
||||
let resultant ← mvarId.getType
|
||||
|
@ -95,11 +95,11 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (List Meta.Inductio
|
|||
mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
|
||||
newMVars := newMVars ++ [goalConduit]
|
||||
|
||||
return newMVars.toList.map (λ mvar => { mvarId := mvar.mvarId!})
|
||||
return newMVars.map (λ mvar => { mvarId := mvar.mvarId!})
|
||||
|
||||
def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
||||
let recursor ← Elab.Term.elabTerm (stx := stx) .none
|
||||
let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
|
||||
Elab.Tactic.setGoals $ nextGoals.map (·.mvarId)
|
||||
Elab.Tactic.setGoals $ nextGoals.toList.map (·.mvarId)
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -24,8 +24,8 @@ def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
|
|||
|
||||
structure BranchResult where
|
||||
fvarId?: Option FVarId := .none
|
||||
main: MVarId
|
||||
branch: MVarId
|
||||
main: MVarId
|
||||
|
||||
def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.have
|
||||
|
@ -47,8 +47,8 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
|
|||
|
||||
return {
|
||||
fvarId? := .some fvarId,
|
||||
main := mvarUpstream.mvarId!,
|
||||
branch := mvarBranch.mvarId!,
|
||||
main := mvarUpstream.mvarId!,
|
||||
}
|
||||
|
||||
def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
|
||||
|
@ -74,8 +74,8 @@ def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult
|
|||
pure mvarUpstream
|
||||
|
||||
return {
|
||||
main := mvarUpstream.mvarId!,
|
||||
branch := mvarBranch.mvarId!,
|
||||
main := mvarUpstream.mvarId!,
|
||||
}
|
||||
|
||||
def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
|
||||
|
|
Loading…
Reference in New Issue