resource lib name changed

This commit is contained in:
aarne
2007-12-12 20:30:11 +00:00
parent f472bf266c
commit 4ea58bce2c
741 changed files with 0 additions and 0 deletions

View File

@@ -0,0 +1,31 @@
resource DemRes = open Prelude in {
oper
Point : Type =
{point : Str} ;
point : Point -> Str = \p ->
p.point ;
mkPoint : Str -> Point = \s ->
{point = s} ;
noPoint : Point =
mkPoint [] ;
concatPoint : (x,y : Point) -> Point = \x,y ->
mkPoint (point x ++ point y) ;
-- A type is made demonstrative by adding $Point$.
Dem : Type -> Type = \t -> t ** Point ;
mkDem : (t : Type) -> t -> Point -> Dem t = \_,x,s ->
x ** s ;
nonDem : (t : Type) -> t -> Dem t = \t,x ->
mkDem t x noPoint ;
}