Resolve "Add axioms" ✨️
Closes #70 🐔️👍️ Approved-by:v-lafeychine <vincent.lafeychine@proton.me> Approved-by:
loutr <loutr@crans.org> Approved-by:
aalbert <augustin.albert@bleu-azure.fr> 🦀️
🍰 🦀️🍰 🦀️🍰 * fix: change lifetime in functions for axiom-term construction * docs: refer to payloads in builder documentation when missing item documentation * Apply 1 suggestion(s) to 1 file(s) * Apply 1 suggestion(s) to 1 file(s) * chore(kernel): remove unused pointer * Apply 1 suggestion(s) to 1 file(s) * Apply 1 suggestion(s) to 1 file(s) * Apply 1 suggestion(s) to 1 file(s) * Apply 1 suggestion(s) to 1 file(s) * Apply 1 suggestion(s) to 1 file(s) * chore(kernel): remove unused file * chore(kernel): coverage * chore(kernel):add coverage * fix(kernel): fix comment * Apply 1 suggestion(s) to 1 file(s) * chore(kernel): move axiom.rs back to root * feat(kernel): have working axioms * feat(kernel): better Axiom type * fix(kernel): fix memoization issue with WHNF and reductions * chore(proost): make annoying clippy happy * chore(parser): make annoying clippy happy * chore(kernel): make annoying clippy happy * fix(kernel): fix type inference memoization issue with declarations * fix(kernel): seamless builder interface for variable/declarations * fix(kernel): remove unused function * feat(kernel): generalize recursors reductors * fix(parser): parsing of vars * fix(kernel): recursor reduction * fix(parser):tests * Revert "feat(all): remove `Var` builder" This reverts commit 9380961f. * feat(kernel): add recursor reduction * feat(kernel): add axiom declarations * chore(parser): remove outdated TODO * chore(kernel): add TODO * feat(kernel): add type-checking for axioms * feat(kernel): add axiom constructor * feat(all): remove `Var` builder * fix(kernel): add axiom constructor
Showing
- kernel/src/axiom.rs 117 additions, 0 deletionskernel/src/axiom.rs
- kernel/src/calculus/term.rs 92 additions, 8 deletionskernel/src/calculus/term.rs
- kernel/src/error.rs 5 additions, 5 deletionskernel/src/error.rs
- kernel/src/lib.rs 4 additions, 6 deletionskernel/src/lib.rs
- kernel/src/memory/arena.rs 21 additions, 0 deletionskernel/src/memory/arena.rs
- kernel/src/memory/declaration/builder.rs 23 additions, 4 deletionskernel/src/memory/declaration/builder.rs
- kernel/src/memory/declaration/mod.rs 3 additions, 3 deletionskernel/src/memory/declaration/mod.rs
- kernel/src/memory/level/builder.rs 17 additions, 5 deletionskernel/src/memory/level/builder.rs
- kernel/src/memory/level/mod.rs 5 additions, 4 deletionskernel/src/memory/level/mod.rs
- kernel/src/memory/term/builder.rs 43 additions, 11 deletionskernel/src/memory/term/builder.rs
- kernel/src/memory/term/mod.rs 17 additions, 9 deletionskernel/src/memory/term/mod.rs
- kernel/src/type_checker.rs 41 additions, 25 deletionskernel/src/type_checker.rs
- parser/src/command/parse.rs 12 additions, 18 deletionsparser/src/command/parse.rs
- parser/src/error.rs 3 additions, 3 deletionsparser/src/error.rs
- proost/src/error.rs 4 additions, 1 deletionproost/src/error.rs
- proost/src/evaluator.rs 28 additions, 0 deletionsproost/src/evaluator.rs
- proost/src/main.rs 12 additions, 1 deletionproost/src/main.rs
- proost/src/rustyline_helper.rs 17 additions, 4 deletionsproost/src/rustyline_helper.rs
Loading
Please register or sign in to comment