Open pchiusano opened 2 years ago
Here's a smaller test case:
doc1 = {{
@typecheck ```
oa : Set Text
oa = Set.fromList ["alice", "bob", "carol"]
contains "alice" oa
```
@typecheck ```
recur : [Nat] -> Nat
recur = cases
[] -> 0
[n] -> n
ns ->
(l,r) = halve ns
recur l + recur r
```
}}
Has something to do with floating things in the first snippet. Note that switching the order of the snippets avoids the problem.
I think this might no longer be relevant, because there is no more 'local recursive' floating. At least, my 'smallter test case' no longer causes an error.
And then do
display article
, which yieldsThe doc in question has some embedded definitions. I could convert them to use
@source
instead, so I'm not blocked, but I thought this would make a decent bug report since it would be nice if this worked.