File tree Expand file tree Collapse file tree 4 files changed +8
-8
lines changed
Expand file tree Collapse file tree 4 files changed +8
-8
lines changed Original file line number Diff line number Diff line change @@ -23,8 +23,8 @@ example (m n : Nat) : (↑m : Int) < 0 ∧ (↑n : Int) > 0 := by
2323 set_option aesop.check.script false in
2424 aesop (config := { enableSimp := false , warnOnNonterminal := false })
2525 all_goals
26- guard_hyp fwd : 0 ≤ (n : Int)
27- guard_hyp fwd_1 : 0 ≤ (m : Int)
26+ guard_hyp fwd : 0 ≤ (m : Int)
27+ guard_hyp fwd_1 : 0 ≤ (n : Int)
2828 falso
2929
3030@[aesop safe forward (pattern := min x y)]
@@ -44,8 +44,8 @@ axiom triangle (a b : Int) : |a + b| ≤ |a| + |b|
4444
4545example : |a + b| ≤ |c + d| := by
4646 aesop!
47- guard_hyp fwd_1 : |a + b| ≤ |a| + |b|
48- guard_hyp fwd : |c + d| ≤ |c| + |d|
47+ guard_hyp fwd : |a + b| ≤ |a| + |b|
48+ guard_hyp fwd_1 : |c + d| ≤ |c| + |d|
4949 falso
5050
5151@[aesop safe apply (pattern := (0 : Nat))]
Original file line number Diff line number Diff line change 55 "type" : " git" ,
66 "subDir" : null ,
77 "scope" : " " ,
8- "rev" : " 973f2658ea854c89067bc6be53339ba143c9bcef " ,
8+ "rev" : " 08681ddeb7536a50dea8026c6693cb9b07f01717 " ,
99 "name" : " batteries" ,
1010 "manifestFile" : " lake-manifest.json" ,
11- "inputRev" : " v4.21.0-rc2 " ,
11+ "inputRev" : " v4.21.0-rc3 " ,
1212 "inherited" : false ,
1313 "configFile" : " lakefile.toml" }],
1414 "name" : " aesop" ,
Original file line number Diff line number Diff line change @@ -7,7 +7,7 @@ platformIndependent = true
77[[require ]]
88name = " batteries"
99git = " https://github.com/leanprover-community/batteries"
10- rev = " v4.21.0-rc2 "
10+ rev = " v4.21.0-rc3 "
1111
1212[[lean_lib ]]
1313name = " Aesop"
Original file line number Diff line number Diff line change 1- leanprover/lean4:v4.21.0-rc2
1+ leanprover/lean4:v4.21.0-rc3
You can’t perform that action at this time.
0 commit comments