refresh transcripts

This commit is contained in:
Paul Chiusano 2022-12-02 13:53:10 -06:00
parent e89fd61266
commit 96f63a3192
4 changed files with 4 additions and 12 deletions

View File

@ -16,9 +16,5 @@ x = 'f
1 | f : (forall a . a -> a) -> Nat
from right here:
1 | f : (forall a . a -> a) -> Nat
```

View File

@ -98,10 +98,6 @@ ex4 =
2 | [1,2,3] -- no good
from right here:
2 | [1,2,3] -- no good
Note: actions within a block must have type Unit.

View File

@ -47,10 +47,6 @@ h0 req = match req with
1 | h0 : Request {X t} b -> Optional b
from right here:
1 | h0 : Request {X t} b -> Optional b
```
This code should not check because `t` does not match `b`.

View File

@ -89,5 +89,9 @@ hmm = "Not, in fact, a number"
1 | hmm : .builtin.Nat
2 | hmm = "Not, in fact, a number"
from right here:
2 | hmm = "Not, in fact, a number"
```