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

feat: Let tactic #70

Merged
aniva merged 4 commits from goal/let into dev 2024-04-12 21:42:32 -07:00
Conversation 0 Commits 4 Files Changed 3 +9 -4
1 changed files with 9 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit b45b90b810 - Show all commits

13
Test/Proofs.lean
View File

@ -564,20 +564,25 @@ def test_let (specialized: Bool): TestM Unit := do
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[interiorGoal [] "p ∨ ¬p"]) #[interiorGoal [] "p ∨ ¬p"])
let expr := "let b: Nat := _; _"
let letType := "Nat"
let expr := s!"let b: {letType} := _; _"
let result2 ← match specialized with let result2 ← match specialized with
| true => state1.tryLet (goalId := 0) (binderName := "b") (type := "Nat") | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType)
| false => state1.tryAssign (goalId := 0) (expr := expr) | false => state1.tryAssign (goalId := 0) (expr := expr)
let state2 ← match result2 with let state2 ← match result2 with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check expr ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = let serializedState2 ← state2.serializeGoals (options := ← read)
addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
#[ #[
interiorGoal [] "Nat", interiorGoal [] letType,
interiorGoal [] "let b := ?m.20;\np ∨ ¬p" interiorGoal [] "let b := ?m.20;\np ∨ ¬p"
]) ])
-- Check that the goal mvar ids match up
addTest $ LSpec.check expr ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20")
let tactic := "exact a" let tactic := "exact a"
let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with