From 3cf472b13c9b329b711a5c254fc6f89268a99eda Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Mon, 8 Jul 2024 23:59:31 +0200 Subject: implement argument lists for top-level definitions --- test/bool.toytt | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) (limited to 'test') 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) -- cgit 1.4.1