the next generation of the in-browser educational proof assistant

add atom prelude functionality master

this is an mvp to show a way of adding special builtins with access to the internal structure of atoms. the immediate use case is providing a length function on strings, which evaluates to a Nat. this expands quite drastically the set of predicates we're able to describe, because previously there was no way to separate ground parts of a string given that epsilon can unify with anything. it's nice in that there's no need to change any of the signatures, apart from the introduction of `reduce`--- Preludic.Atom simply has `type t = anyValue` and gives a dummy `wrap` definition. where a prelude function can be evaluated syntactically, this evaluation can take place in `parse`, which directly produces the right tag and `anyValue`. where we need to defer evaluation of a prelude function until a concrete substitution has been chosen, we parse into a two-dimensional anyValue: ``` length("$s") │ │parse() │ │ ▼ ┌───────────────┐ sub(0 -> [a b])┌───────────────┐ reduce() ┌────────────┐ │ PreludeTag ├───────────────►│ PreludeTag ├─────────────►│ NatTag │ └───────┬───────┘ └───────────────┘ └─────┬──────┘ │ │ │ │ │ │ │ │ │ ┌───────┴───────┐ ┌───────┴───────┐ ┌──────────────┐ │ LengthTag │ │ LengthTag │ │ 2 │ └───────┬───────┘ └───────┬───────┘ └──────────────┘ │ │ │ │ │ │ ┌───────┴───────┐ ┌───────┴───────┐ │[Var({idx: 0})]│ │ [ a, b] │ └───────────────┘ └───────────────┘ ```


Author Josh Brown Date Commit ba2925d8 Parent 8b511217 Change ID vmrlysln