diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/bool.toytt | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/test/bool.toytt b/test/bool.toytt index c8e62fd..5f16d20 100644 --- a/test/bool.toytt +++ b/test/bool.toytt @@ -1,11 +1,13 @@ -def not : bool -> bool := - \x -> bool-elim x at _ -> bool [ +def id (A : type) (x : A) : A := x + +def not (x : bool) : bool := + bool-elim x at _ -> bool [ true => false, false => true ] -def and : bool -> bool -> bool := - \x -> \y -> bool-elim x at _ -> bool [ +def and (x : bool) (y : bool) : bool := + bool-elim x at _ -> bool [ true => bool-elim y at _ -> bool [ true => true, false => false @@ -13,8 +15,8 @@ def and : bool -> bool -> bool := false => false ] -def or : bool -> bool -> bool := - \x -> \y -> bool-elim x at _ -> bool [ +def or (x : bool) (y : bool) : bool := + bool-elim x at _ -> bool [ true => true, false => bool-elim y at _ -> bool [ true => true, @@ -22,7 +24,6 @@ def or : bool -> bool -> bool := ] ] -def xor : bool -> bool -> bool := - \x -> \y -> or - (and x (not y)) - (and (not x) y) +def xor (x : bool) (y : bool) : bool := + or (and x (not y)) + (and (not x) y) |