Skip to content

Commit f2e0e14

Browse files
author
Petar Maksimovic
committed
bringing back stop
1 parent 2d15329 commit f2e0e14

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

SP1Operations/Compare/LtOperationSigned.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -158,6 +158,7 @@ lemma spec.branch
158158
simp_all
159159
repeat rw [eq_comm (a := 1)] at *; symm at lt_05 lt_06
160160
constructor <;> intro sgn <;> (repeat rw [this]) <;> clear this <;> simp_all
161+
stop
161162
. rcases h_flag_0_bool <;> rcases h_flag_1_bool <;>
162163
rcases h_flag_2_bool <;> rcases h_flag_3_bool <;>
163164
-- FIXME: `split_ands` hangs; `try_constructor` hangs

0 commit comments

Comments
 (0)