correctly distinguish between fun and data judgements

This commit is contained in:
krangelov
2021-11-18 13:50:09 +01:00
parent 7ff38bfcbe
commit 06980404a9
27 changed files with 59 additions and 332 deletions

View File

@@ -0,0 +1,19 @@
concrete basic_cnc of basic = open Prelude in {
lincat N = {s : Str; is_zero : Bool} ;
lincat S = Str ;
lin z = {s="0"; is_zero=True} ;
s n = {
s = case n.is_zero of {
True => "1" ;
False => n.s ++ "+" ++ "1"
} ;
is_zero = False
} ;
lin c n = n.s ;
lincat P = {};
}