Changes between Version 7 and Version 8 of TypeNats/Basics

Timestamp:

01/16/11 09:40:04 (2 years ago)

Author:

diatchki

Comment:

--

TypeNats/Basics

@@ -20 +20 @@
 natToInteger :: Nat n -> Integer
 }}}
-The only value of type {{{Nat n}}} is the number {{{n}}}.  (Technically, there is also an undefined element.)
+The only "interesting" value of type ''Nat n'' is the number ''n''.  Technically, there is also an undefined element.
 
+One may think of the smart constructor ''nat'' as being a method of a special built-in class:
 {{{
 class NatI n where
   nat :: Nat n
 
-instance NatI 0 where nat = "0"
-instance NatI 1 where nat = "1"
-instance NatI 2 where nat = "2"
+instance NatI 0 where nat = "singleton 0 value"
+instance NatI 1 where nat = "singleton 1 value"
+instance NatI 2 where nat = "singleton 2 value"
 etc.
 }}}