preserve 1.0

This commit is contained in:
aarne
2006-06-22 22:27:48 +00:00
parent 251bc4c738
commit 4821244741
569 changed files with 0 additions and 0 deletions

View File

@@ -1,31 +0,0 @@
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 ;
}