the next generation of the in-browser educational proof assistant
1type rec t =
2 | Symbol({name: string, constructor: bool})
3 | Var({idx: int})
4 | Schematic({schematic: int})
5 | Lam({name: string, body: t})
6 | App({func: t, arg: t})
7 // Unallowed is used internally in unify, where Nipkow 1993 uses Var(-infinity)
8 | Unallowed
9
10include Signatures.TERM
11 with type t := t
12 and type meta = string
13 and type schematic = int
14 and type subst = Belt.Map.Int.t<t>
15
16let emptySubst: subst
17let strip: t => (t, array<t>)
18let app: (t, array<t>) => t
19let mkvars: int => array<t>
20let mapTerms: (t, t => t) => t
21// exposed for testing purposes
22exception UnifyFail(string)
23let substAdd: (subst, schematic, t) => subst
24let unifyTerm: (t, t, subst, ~gen: option<gen>) => subst
25let reduceSubst: subst => subst
26let rewrite: (t, t, t, ~subst: subst, ~gen: option<gen>) => (subst, t)