~thon/thon

ref: 96d1b14e2711279bf716346de06d1ccda3508cea thon/examples/auto-natlist.thon -rw-r--r-- 191 bytes
96d1b14eEvan Bergeron More 3 months ago
                                                                                
1
2
3
4
5
6
7
data list = nil unit | cons nat * list in
fun isempty : list -> nat =
  \ natlist : list ->
  case exposelist natlist of
      empty -> S Z
    | not -> Z
in (isempty (cons (Z, (nil unit))))