Use Prop for Boogie bool type

boogie-org · Jan 27, 2025 · c8fda07 · c8fda07
1 parent bf2dab8
commit c8fda07
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/LeanBoogie/ConTy.lean b/LeanBoogie/ConTy.lean
@@ -46,7 +46,7 @@ abbrev TyA : Ty -> Type
 | .unit => Unit
 | .int => Int
 | .real => Real
-| .bool => Bool
+| .bool => Prop
 | .bv bits => BitVec bits
 | .map A B => TyA A -> TyA B
 
@@ -57,7 +57,7 @@ def TyA.inhabited : {A : Ty} -> A
 | .unit => default
 | .int => default
 | .real => default
-| .bool => default
+| .bool => True
 | .bv _ => default
 | .map _ _ => fun _ => inhabited
 

diff --git a/LeanBoogie/Effect/Mem.lean b/LeanBoogie/Effect/Mem.lean
@@ -49,5 +49,5 @@ private def i : Var Γ .int := .v0
 private def b : Var Γ (.bv32) := .v1
 private def f : Var Γ (.bool ~> .int) := .v2
 private example : ITree (Mem Γ) Unit := do
-  let fn : Bool -> Int <- Mem.read f
+  let fn : Prop -> Int <- Mem.read f
   Mem.write b (fn false)