holbert-ng
the next generation of the in-browser educational proof assistant
Star
Fork
Watch

Commits on main

Liam O’Connor
migrate to forester 6.0
committed
Liam O'Connor
performance issues fixed, forest refactoring
committed
Liam O'Connor
prettier settings block
committed
Liam O'Connor
more cosmetic improvement
committed
Liam O'Connor
presentation and build improvements
committed
Liam O'Connor
fairly decent sidebar behaviour now.
committed
Liam O'Connor
started work on the sidebar
committed
Liam O'Connor
add tree and summary views to proofs
committed
Liam O'Connor
fix notification/updating bugs
committed
Liam O'Connor
The term syntax overhaul: mixfix parser and pretty printer
committed
Liam O'Connor
add (currently no-op) display tabs.
committed
Liam O'Connor
deleteable proof steps, refactoring
committed
Liam O'Connor
add editable metas and rule names to proofs
committed
Liam O'Connor
some basic handling of shadowed assumptions
committed
Liam O'Connor
fix build problems
committed
Liam O'Connor
SHOTerm is now HOTerm
committed
Liam O'Connor
add constructor support to SHOTerm
committed
Liam O'Connor
rewriting is now term-generic.
committed
Liam O'Connor
A rewriting method for SHOTerms
committed
Liam O'Connor
updated forest
committed
Liam O'Connor
make SHOTerm handle induction solutions, port InductiveSet to SHOTerm
committed
Liam O'Connor
remove some random notes
committed
Liam O'Connor
add the experimental forest
committed
Liam O'Connor
fixing bugs. added “simple ho terms” because I can’t debug HOTerm.
committed
Liam O’Connor
add reset buttons, miscellaneous bugfixes
committed
Liam O’Connor
better proof view in the forester integration
committed
Liam O’Connor
multi-doc forester integration, wip
committed
aesthetic changes
committed
fix a_1-unification
committed
minimal failing unit test
committed
HOTerm atom fixes
committed
add atom prelude functionality
committed
initial associative-commutative atom definition
committed
reorganise atom defns
committed
chore: npm update
committed
Atom for HOTerm
committed
Liam O’Connor
Merge branch 'main' of tangled.org:liamoc.net/holbert-ng
committed
add sub-menu for introduction rules with more than 1 sub
committed
format Method.res
committed
renames
committed
functorise StringAxiomSet
committed
move to list-based combine atom functor rather than sum tree
committed
clean ATOM/BASE_ATOM signature
committed
Liam O’Connor
testing CI with this commit
committed
port github CI to tangled
committed
Liam O'Connor
adding hierarchical method menus
committed
Liam O'Connor
Merge pull request #8 from joshcbrown/push-urxktozzxxlq
committed
improve parsing error messages with expects clause
committed
fix parser lib
committed
implement sexp parser with new lib
committed
lay foundations for parser
committed
Liam O'Connor
Merge pull request #27 from joshcbrown/atom-combine-coerce
committed
Liam O'Connor
Merge pull request #26 from joshcbrown/atom-subst-cleaning
committed
fix value wrapping
committed
simplify coercions
committed
convert SExp lowerings to coercions
committed
renames
committed
introduce foreign to lazily evaluate conversion
committed
coercions b/w atoms rather than intermediaries
committed
reorganise
committed