~thon/thon

a9a66ca55d21bea37851711d6baa645672066e51 — Evan Bergeron 8 months ago e1c37a8
Use the nicer syntax
1 files changed, 7 insertions(+), 6 deletions(-)

M examples/nilisempty.thon
M examples/nilisempty.thon => examples/nilisempty.thon +7 -6
@@ 1,10 1,11 @@
let isempty : (u l. (unit |  (nat * l))) -> nat =
    \ natlist : (u l. (unit |  (nat * l))) ->
fun isempty : (data l = (unit | nat * l)) -> nat =
  \ natlist : (data l = (unit | nat * l)) ->
        (case (unfold natlist) of
           empty -> S Z
         | hdAndTl -> Z)
in let nil : (u l. (unit |  (nat * l))) =
    fold u l. (unit | (nat * l))
    with left unit : (unit |  (nat * (u l. (unit | (nat * l)))))
         | not -> Z)
in let nil : (data l = (unit | nat * l)) =
    fold data l = (unit | nat * l) with
    left unit : (unit
               | nat * (data l = (unit | nat * l)))
in
(isempty nil)