Repository navigation
v1.0.15
What's Changed
- Exploratory work on stateless translation of LN into Named by @h0nzZik in #341
- Another exploratory work on LN2Named translation by @h0nzZik in #342
- Refactorings around the Deduction theorem; mlClassic by @h0nzZik in #343
- update nixpkgs; coq 8.17 by @h0nzZik in #345
- Slightly generalize DT by @h0nzZik in #344
- Named UI: preliminaries by @h0nzZik in #347
- Transitivity of ML subseteq by @h0nzZik in #348
- Initial work on Contextual implication by @h0nzZik in #349
- Freshness Manager by @h0nzZik in #350
- Use FreshnessManager in the FO proof mode by @h0nzZik in #360
- Fix nonterminating tactics by @berpeti in #371
- Product sorts (and some other things) by @h0nzZik in #372
- Evaluation with better examples by @berpeti in #369
- make the ProofMode tutorial work again by @h0nzZik in #373
- automatically introduce wf premises when entering proof mode by @h0nzZik in #374
Full Changelog: v1.0.14...v1.0.15