mio19.uk / holbert-ng
the next generation of the in-browser educational proof assistant
Star
Fork 0
Watch

Commits on main

Migrate to ReScript 13 main
Mio committed
Revert "minimal failing unit test"
Mio committed
aesthetic changes
Josh Brown committed
fix a_1-unification
Josh Brown committed
minimal failing unit test
Josh Brown committed
HOTerm atom fixes
Josh Brown committed
add atom prelude functionality
Josh Brown committed
initial associative-commutative atom definition
Josh Brown committed
reorganise atom defns
Josh Brown committed
chore: npm update
Mio committed
Atom for HOTerm
Mio committed
Merge branch 'main' of tangled.org:liamoc.net/holbert-ng
Liam O’Connor committed
add sub-menu for introduction rules with more than 1 sub
Josh Brown committed
format Method.res
Josh Brown committed
renames
Josh Brown committed
functorise StringAxiomSet
Josh Brown committed
move to list-based combine atom functor rather than sum tree
Josh Brown committed
clean ATOM/BASE_ATOM signature
Josh Brown committed
testing CI with this commit
Liam O’Connor committed
port github CI to tangled
Josh Brown committed
adding hierarchical method menus
Liam O'Connor committed
Merge pull request #8 from joshcbrown/push-urxktozzxxlq
Liam O'Connor committed
improve parsing error messages with expects clause
Josh Brown committed
fix parser lib
Josh Brown committed
implement sexp parser with new lib
Josh Brown committed
lay foundations for parser
Josh Brown committed
Merge pull request #27 from joshcbrown/atom-combine-coerce
Liam O'Connor committed
Merge pull request #26 from joshcbrown/atom-subst-cleaning
Liam O'Connor committed
fix value wrapping
Josh Brown committed
simplify coercions
Josh Brown committed
convert SExp lowerings to coercions
Josh Brown committed
renames
Josh Brown committed
introduce foreign to lazily evaluate conversion
Josh Brown committed
coercions b/w atoms rather than intermediaries
Josh Brown committed
reorganise
Josh Brown committed
checkpoint
Josh Brown committed
combine atom functor
Josh Brown committed
add example showing type coercion failure
Josh Brown committed
add checks for substitution failure
Josh Brown committed
adjust atom substDeBruijn sig
Josh Brown committed
Merge pull request #25 from joshcbrown/string-in-sexp
Liam O'Connor committed
tidy further
Josh Brown committed
remove ghost, tidy
Josh Brown committed
rename unifyWithAnything -> concrete
Josh Brown committed
slightly neater workaround for sexp functor
Josh Brown committed
remove (some of) atom debjruijn sub partiality
Josh Brown committed
rename string term -> string atom
Josh Brown committed
rename symbol -> atom
Josh Brown committed
add upshift to symbol signature
Josh Brown committed
add concrete term method
Josh Brown committed
restore original judgment signature
Josh Brown committed
remove redundant constSymbol function
Josh Brown committed
remove StringTermJudgment
Josh Brown committed
slightly more involved example
Josh Brown committed
lots of fixes
Josh Brown committed
fix (?) string sexp axioms
Josh Brown committed
remove redundant StringTermJudgment
Josh Brown committed
symbol view logic
Josh Brown committed
example
Josh Brown committed
finished?
Josh Brown committed