Skip to content

Commit f6f61b9

Browse files
Remove useless definitions
Notations [^^^?] and [&&&?] are directly introduced by the lean backend
1 parent 33dcc08 commit f6f61b9

File tree

1 file changed

+0
-5
lines changed

1 file changed

+0
-5
lines changed

hax-lib/proof-libs/lean/Hax/Lib.lean

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -238,11 +238,6 @@ infixl:60 " &&&? " => fun a b => pure (HAnd.hAnd a b)
238238
are also provided -/
239239
namespace Rust_primitives.Hax.Machine_int
240240

241-
@[simp, spec]
242-
def bitxor {α} [HXor α α α] (a b: α) : Result α := a ^^^? b
243-
@[simp, spec]
244-
def hax_machine_int_bitand {α} [HAnd α α α] (a b: α) : Result α := a &&&? b
245-
246241
@[simp, spec]
247242
def eq {α} (x y: α) [BEq α] : Result Bool := pure (x == y)
248243
@[simp, spec]

0 commit comments

Comments
 (0)