File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -289,7 +289,7 @@ def test_load_sorry(self):
289289 state0 = unit .goal_state
290290 self .assertEqual (state0 .goals , [
291291 Goal (
292- "_uniq.3 " ,
292+ "_uniq.5 " ,
293293 [Variable (name = "p" , t = "Prop" )],
294294 target = "p → p" ,
295295 ),
@@ -301,15 +301,15 @@ def test_load_sorry(self):
301301 state1b = server .goal_tactic (state0 , tactic = TacticDraft ("by\n have h1 : Or p p := sorry\n sorry" ))
302302 self .assertEqual (state1b .goals , [
303303 Goal (
304- "_uniq.17 " ,
304+ "_uniq.19 " ,
305305 [Variable (name = "p" , t = "Prop" )],
306306 target = "p ∨ p" ,
307307 ),
308308 Goal (
309- "_uniq.19 " ,
309+ "_uniq.21 " ,
310310 [
311311 Variable (name = "p" , t = "Prop" ),
312- Variable (name = "h1" , t = "p ∨ p" , v = "?m.17 " ),
312+ Variable (name = "h1" , t = "p ∨ p" , v = "?m.19 " ),
313313 ],
314314 target = "p → p" ,
315315 ),
@@ -321,7 +321,7 @@ def test_distil_search_target(self):
321321 state0 = unit .goal_state
322322 self .assertEqual (state0 .goals , [
323323 Goal (
324- "_uniq.1 " ,
324+ "_uniq.3 " ,
325325 [],
326326 target = "∀ (p : Prop), p → p" ,
327327 ),
You can’t perform that action at this time.
0 commit comments