aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

chore: Version 0.3 #136

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

6
Pantograph/Frontend/Elab.lean
View File

@ -1,4 +1,3 @@
/- Adapted from https://github.com/semorrison/lean-training-data -/
import Lean.Elab.Import import Lean.Elab.Import
import Lean.Elab.Command import Lean.Elab.Command
import Lean.Elab.InfoTree import Lean.Elab.InfoTree
@ -16,6 +15,7 @@ namespace Pantograph.Frontend
-- Info tree filtering functions -- Info tree filtering functions
/- Adapted from lean-training-data -/
structure TacticInvocation where structure TacticInvocation where
info : Elab.TacticInfo info : Elab.TacticInfo
ctx : Elab.ContextInfo ctx : Elab.ContextInfo
@ -107,10 +107,12 @@ structure InfoWithContext where
private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
let infos ← t.findAllInfoM none fun i ctx? => match i with let infos ← t.findAllInfoM none fun i ctx? => match i with
| .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
let .some expectedType := expectedType? | return (false, true)
let .some ctx := ctx? | return (false, true) let .some ctx := ctx? | return (false, true)
if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
if expectedType?.isNone then
throw $ .userError "Sorry of indeterminant type is not allowed"
return (true, false) return (true, false)
let .some expectedType := expectedType? | return (false, true)
let typeMatch ← ctx.runMetaM lctx do let typeMatch ← ctx.runMetaM lctx do
let type ← Meta.inferType expr let type ← Meta.inferType expr
Meta.isExprDefEqGuarded type expectedType Meta.isExprDefEqGuarded type expectedType