Modules§
- pretty 🔒
Structs§
- An existential varriable is identified by a context and an id. Two evars are considered equal if both the context and id are equal.
- EVar
Ctxt 🔒 - A generator of evars. Evars are associated with a context. Contexts are visited in a stack-like fashion. When entering a context data can be associated to that particular context. When a context is exited, all its evars are put in a list of pending contexts. No more evars can be generated for pending contexts, but they can still be unified. At any point, pending contexts can be solved, returning a solution for all of their evars or an error if some evar hasn’t been unified yet.
- EVid 🔒Existential variable id