Jon Sterling

Currently, `SYMBOL.named` is used; we need to use `SYMBOL.fresh ctx` instead.

Or, `sml-nominal-algebra` or `sml-nominal-syntax`?

When we begin to tune performance and try out things like hash-consing, we'll need to have a benchmark in place.

Sadly, the `SORT` signature is part of `cmlib`, so it's kind of inconvenient if we use it here. ~~I think a better option would be to just collapse the whole...

Support @string

1

It would be great to support the `@string` bibtex declaration, and handle expansion.

This resolves #1, as well as another issue I noticed where the congruences for `app` and `lam` were insufficiently constrained.

https://github.com/jmchapman/TT-in-TT/blob/master/2DSyntax.agda#L61 ``` agda trans : ∀{Γ Δ}{γ γ' γ'' : Sub Γ Δ} → γ' ≡Sub γ'' → γ ≡Sub γ' → γ' ≡Sub γ'' ``` should be ``` agda...

We found that backtracking was basically useless in practice for RedPRL, because the state space would just blow up. I'm thinking that it actually may be a bad idea, and...

I want to try out alternative representations of the proof that that would avoid premature substitutions; but to do this, I need to somehow make the proof state abstract so...