~thon/thon

49cadea3a25d3d8c7aa708652a8bc1ddf929d246 — Evan Bergeron 8 months ago 2d167c2
Update README
5 files changed, 6 insertions(+), 4 deletions(-)

M README.md
A examples/.#impl.thon
A examples/.#impl2.thon
A examples/aeqv.thon
A examples/all.thon
M README.md => README.md +0 -4
@@ 117,10 117,6 @@ you didn't write this code, it's not your fault it does it this way).
 (*get*) \ tup : (nat * nat) -> fst tup)
```

(Disclaimer, the syntax here needs to be fixed a bit still, it was
made before there were variable names and so now I need to thread a
couple more names through...)

Now each of these implementations can be packed away with the syntax

```

A examples/.#impl.thon => examples/.#impl.thon +1 -0
@@ 0,0 1,1 @@
evan@xone.55553:1601838966
\ No newline at end of file

A examples/.#impl2.thon => examples/.#impl2.thon +1 -0
@@ 0,0 1,1 @@
evan@xone.55553:1601838966
\ No newline at end of file

A examples/aeqv.thon => examples/aeqv.thon +3 -0
@@ 0,0 1,3 @@
ifz Z of
  Z -> poly t -> (Z)
| S p -> poly s -> (Z)

A examples/all.thon => examples/all.thon +1 -0
@@ 0,0 1,1 @@
(poly t -> poly s -> \ x : (t -> (some v . (s->v))) -> x)