GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-05-11 20:22:51 -06:00
Code Issues Packages Projects Releases Wiki Activity

Changed all example programs to use layout syntax.

Browse Source
This commit is contained in:
bringert
2005-11-28 21:45:22 +00:00
parent 5a82068ddc
commit 02c23401a7
10 changed files with 83 additions and 90 deletions
Download Patch File Download Diff File Expand all files Collapse all files

24
transfer/examples/list.tr
View File

@@ -1,17 +1,17 @@
import nat ;
import nat
data List : (_:Type) -> Type where
{ Nil : (A:Type) -> List A ;
Cons : (A:Type) -> A -> List A -> List A ; } ;
Nil : (A:Type) -> List A
Cons : (A:Type) -> A -> List A -> List A
size : (A:Type) -> List A -> Nat ;
size _ (Nil _) = Zero ;
size A (Cons _ x xs) = Succ (size A xs) ;
size : (A:Type) -> List A -> Nat
size _ (Nil _) = Zero
size A (Cons _ x xs) = Succ (size A xs)
map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B ;
map _ B _ (Nil _) = Nil B ;
map A B f (Cons _ x xs) = Cons B (f x) (map A B f xs) ;
map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B
map _ B _ (Nil _) = Nil B
map A B f (Cons _ x xs) = Cons B (f x) (map A B f xs)
append : (A:Type) -> (xs:List A) -> List A -> List A ;
append _ (Nil _) ys = ys ;
append A (Cons _ x xs) ys = Cons A x (append A xs ys) ;
append : (A:Type) -> (xs:List A) -> List A -> List A
append _ (Nil _) ys = ys
append A (Cons _ x xs) ys = Cons A x (append A xs ys)