~thon/thon

96d1b14e2711279bf716346de06d1ccda3508cea — Evan Bergeron 4 months ago 646b3dd
More
2 files changed, 12 insertions(+), 12 deletions(-)

M README.md
M examples/auto-natlist.thon
M README.md => README.md +5 -5
@@ 4,13 4,13 @@ thon is a small programming language. Here's an example program that
verifies the singleton list is not empty.

```
data list = Nil unit | Cons nat * list in
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))))
  case exposelist natlist of
      empty -> S Z
    | not -> Z
in (isempty (cons (Z, (nil unit))))
```

thon has natural numbers, functions, recursion, binary product and sum

M examples/auto-natlist.thon => examples/auto-natlist.thon +7 -7
@@ 1,7 1,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))
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))))