forked from GitHub/gf-core
Move transfer into the GF repo.
This commit is contained in:
8
transfer/examples/bool.tr
Normal file
8
transfer/examples/bool.tr
Normal file
@@ -0,0 +1,8 @@
|
||||
data Bool : Type where { True : Bool; False : Bool; } ;
|
||||
|
||||
depif : (A:Type) -> (B:Type) -> (b:Bool) -> A -> B -> if Type b then A else B ;
|
||||
depif _ _ True x _ = x ;
|
||||
depif _ _ False _ y = y ;
|
||||
|
||||
not : Bool -> Bool ;
|
||||
not b = if b then False else True ;
|
||||
Reference in New Issue
Block a user