~thon/thon

ref: 646b3dd8476232930872ac776c0a5a07d3472f32 thon/examples/auto-natlist.thon -rw-r--r-- 199 bytes
646b3dd8Evan Bergeron Update README 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 (Nil unit))