feat: Elementarized tactics with motives, congruence, and absurdity #72

Merged
aniva merged 41 commits from goal/mapply into dev 2024-06-12 13:52:46 -07:00
2 changed files with 3 additions and 5 deletions
Showing only changes of commit bd42c396d7 - Show all commits

View File

@ -70,11 +70,10 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
let pending ← mvarIdPending.withContext do
let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
--IO.println s!"{padding}├Pre: {inner}"
let r := (← Expr.abstractM inner fvars).instantiateRev args
pure r
pure <| (← inner.abstractM fvars).instantiateRev args
-- Tail arguments
let result := mkAppN pending (List.drop fvars.size args.toList |>.toArray)
let result := mkAppRange pending fvars.size args.size args
--IO.println s!"{padding}├MD {result}"
return .done result
else

View File

@ -212,11 +212,10 @@ inductive TacticExecute where
def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): Lean.CoreM TacticResult :=
runTermElabM do
state.restoreElabM
let tactic := match tacticExecute with
state.execute goalId $ match tacticExecute with
| .congruenceArg => Tactic.congruenceArg
| .congruenceFun => Tactic.congruenceFun
| .congruence => Tactic.congruence
state.execute goalId tactic