GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-05-16 14:42:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

Move transfer into the GF repo.

Browse Source
This commit is contained in:
bringert
2005-11-25 16:36:19 +00:00
parent fe2731e5f8
commit dbe8e61acc
42 changed files with 7400 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

23
transfer/examples/nat.tr Normal file
View File

@@ -0,0 +1,23 @@
data Nat : Type where {
Zero : Nat ;
Succ : (n:Nat) -> Nat ;
} ;
plus : Nat -> Nat -> Nat ;
plus Zero y = y ;
plus (Succ x) y = Succ (plus x y) ;
pred : Nat -> Nat ;
pred Zero = Zero ;
pred (Succ n) = n ;
natToInt : Nat -> Int ;
natToInt Zero = 0 ;
natToInt (Succ n) = 1 + natToInt n ;
plus : Nat -> Nat -> Nat ;
plus Zero y = y ;
plus (Succ x) y = Succ (plus x y) ;
intToNat : Int -> Nat ;
intToNat n = if n == 0 then Zero else Succ (intToNat (n-1)) ;