summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
authorSon HO2023-12-14 16:49:34 +0100
committerGitHub2023-12-14 16:49:34 +0100
commitc3e0b90e422cbd902ee6d2b47073940c0017b7fb (patch)
tree92da14273eb068bcf418a2bdf9fbb6d27ba86102 /backends/lean/Base
parentc6247e0c103cc1dc95c2a63ae01602c4a1208dc4 (diff)
parentb32fd66b71ad8fe28449d87a2e0334fdd36e286a (diff)
Merge pull request #53 from AeneasVerif/son/casts
Add support for casts between integers and booleans
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean4
1 files changed, 4 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index db522df2..a8eda6d5 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -411,6 +411,10 @@ def Scalar.or {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty :=
def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Result (Scalar tgt_ty) :=
Scalar.tryMk tgt_ty x.val
+-- This can't fail, but for now we make all casts faillible (easier for the translation)
+def Scalar.cast_bool (tgt_ty : ScalarTy) (x : Bool) : Result (Scalar tgt_ty) :=
+ Scalar.tryMk tgt_ty (if x then 1 else 0)
+
-- The scalar types
-- We declare the definitions as reducible so that Lean can unfold them (useful
-- for type class resolution for instance).