Skip to content

Commit

Permalink
bad PR
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Sep 5, 2024
1 parent c346f81 commit a526fb9
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions ulib/FStar.Math.Lemmas.fsti
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@ module FStar.Math.Lemmas

open FStar.Mul

let _ = assert False

(* Lemma: definition of Euclidean division *)
val euclidean_div_axiom: a:int -> b:pos -> Lemma
(a - b * (a / b) >= 0 /\ a - b * (a / b) < b)
Expand Down

0 comments on commit a526fb9

Please sign in to comment.