Idris2/tests/ttimp/basic006
Edwin Brady 45fc100f6c Store postponed unification problems as values
We stored them as equations between terms, I think because terms are
easy to re-evaluate with new information, and because I thought we might
want to save them out. It's not usually a problem to do that. However...
Going back and forth between terms and values can be expensive if
we're stuck in the middle of a complicated unification problem, the like
of which can turn up a lot if your types are complicated. So, we need to
be able to handle this.
Now store the postponed problems as NF, rather than Term, and add a
fuction to resume evaluating a NF with an updated context.
2021-05-15 20:03:33 +01:00
..
Ambig.yaff fixed whitespace for *.idr,*.ipkg,*.tex,*.yaff, and *.lidr 2021-01-22 15:08:49 +00:00
expected Store postponed unification problems as values 2021-05-15 20:03:33 +01:00
input Add test script 2020-05-19 18:25:18 +01:00
run Add test script 2020-05-19 18:25:18 +01:00