aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 2 Packages Projects Releases Wiki Activity

chore: Version 0.3 #136

Open
aniva wants to merge 600 commits from dev into main
pull from: dev
merge into: aniva:main
Conversation 0 Commits 600 Files Changed 47 +5 -4
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 267290c8f7 - Show all commits

9
Pantograph/Tactic/Assign.lean
View File

@ -28,15 +28,16 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
Elab.Tactic.replaceMainGoal nextGoals Elab.Tactic.replaceMainGoal nextGoals
def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do
Meta.transform src λ Meta.transform src λ expr =>
| .app (.app (.const ``sorryAx ..) type) .. => do if expr.isSorry then do
let type ← instantiateMVars type let type ← instantiateMVars (expr.getArg! 0 |>.bindingBody!)
if type.hasSorry then if type.hasSorry then
throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}" throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}"
let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
modify (mvar.mvarId! :: .) modify (mvar.mvarId! :: .)
pure $ .done mvar pure $ .done mvar
| _ => pure .continue else
pure .continue
-- Given a complete (no holes) expression, extract the sorry's from it and convert them into goals. -- Given a complete (no holes) expression, extract the sorry's from it and convert them into goals.
def draft (goal : MVarId) (expr : Expr) : MetaM (List MVarId) := do def draft (goal : MVarId) (expr : Expr) : MetaM (List MVarId) := do