make things compile

opencompl · Oct 18, 2023 · e4ddae1 · e4ddae1
1 parent 88540c5
commit e4ddae1
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/SSA/Projects/InstCombine/ForMathlib.lean b/SSA/Projects/InstCombine/ForMathlib.lean
@@ -24,7 +24,7 @@ def ofBool : Bool → Bitvec 1 := fun b => b ::ᵥ Vector.nil
 def a : Bitvec 2 := 0
 
 def b : Prop := a ≤ a
-def bb : Bool := b
+def bb : Bool := a ≤ a 
 
 #check b
 def c : Nat := 2

diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
@@ -109,7 +109,7 @@ instance {n} {x y : BitVec n} : Decidable (BitVec.ult x y) :=
 instance {n} {x y : BitVec n} : Decidable (BitVec.ule x y) :=
   decEq _ _
 
-instance {n} {x y : BitVec n} : Decidable (x < y) :=
+instance {n} {x y : BitVec n} : Decidable (x < y) := by
   sorry
 
 instance {n} {x y : BitVec n} : Decidable (x ≤ y) :=