Tree @master (Download .tar.gz)
Commit History
@master
git clone https://git.catseye.tc/Eqthy/
- Keep checkpointing. Tsk at the added axioms. Must address that. Chris Pressey 2 years ago
- Checkpoint converting proof. Chris Pressey 2 years ago
- Introduce update_at_index. Finally fix all_rewrites. Chris Pressey 2 years ago
- Even more checkpointing while hunting down this thing. Chris Pressey 2 years ago
- Checkpoint fixing subst to support checking Socks and Shoes Chris Pressey 2 years ago
- Begin translating Socks and Shoes proof. Add TODO list. Chris Pressey 2 years ago
- Implement Congruence. Chris Pressey 2 years ago
- Stricter syntax for Substitution and Congruence. Chris Pressey 2 years ago
- Implement Substitution based on hint. Chris Pressey 2 years ago
- Begin implementing Substitution based on hint Chris Pressey 2 years ago
- First steps towards handling the derivation-driving hints. Chris Pressey 2 years ago
- Add two failing test cases. They will need to be implemented. Chris Pressey 2 years ago
- Merge branch 'master' of git+ssh://ssh.github.com/catseye/Eqthy Chris Pressey 2 years ago
- Use more consistent nomenclature: the topmost thing is a "document". Chris Pressey 2 years ago
- Add test driver script. Chris Pressey 2 years ago
- Rewrite part of README for clarity, giving the rules of inference. Chris Pressey 2 years ago
- Add example with hints. Chris Pressey 2 years ago
- Parse all defined hints, stub out logic for following them. Chris Pressey 2 years ago
- Consistentify nomenclature: {Program, Source} => Development Chris Pressey 2 years ago
- Add a test case, fix a bug. Chris Pressey 2 years ago
- Partial support for hints. Chris Pressey 2 years ago
- Axioms and theorems can be given names. Chris Pressey 2 years ago
- Add several test cases. Also rewrite the rhs of a step. Chris Pressey 2 years ago
- Fix bug in all_rewrites. All tests pass. flake8. Chris Pressey 2 years ago
- Checkpoint developing all_matches logic. Chris Pressey 2 years ago
- Some rudimentary tests for parsing. Chris Pressey 2 years ago
- Add a rudimentary Falderal test suite with a (failing) test case. Chris Pressey 2 years ago
- Try to rewrite the LHS with every available rule Chris Pressey 2 years ago
- Render objects readably. Derive first step using Reflexivity. Chris Pressey 2 years ago
- Add beginnings of verifier module. Chris Pressey 2 years ago