Kaustuv Chaudhuri
Kaustuv Chaudhuri
The following seems to violate the [principle of least astonishment](https://en.wikipedia.org/wiki/Principle_of_least_astonishment). Kind i type. Type c i. Type f i -> i. Type p i -> prop. Type q i ->...
Currently we do not allow repetitions of `Definition`s and `Theorem`s. This is causing various issues with the IPFS branch that are not worth getting into here. Personally, I see no...
As of 5bb9833e5655039740dadc56ad993f879c7e127b, `Kind` declarations can be repeated with no warnings or errors. Kind n type. Kind n type. % no issues However, `Type` declarations cannot be repeated. Type z...
Todd Wilson (@lambdacalculator) suggests in the Abella mailing list that we should add a `unfold named_clause with ...` form to handle cases such as: ~~~~ %:tapp: of (tapp P E)...
The issue was filed by @ThatDaleMiller here: https://github.com/abella-prover/abella-prover.org/issues/12
Some new examples have been proposed for natural numbers, addition, commutativity, etc. by @lambdacalculator.
- [ ] Abella should output XML or sexps or something that doesn't require guesswork - [ ] Need to remove the dependency on OMake. - [ ] Consider rewriting...
It used to take about 20 seconds to rebuild the entire examples suite prior to 2.0.6. Now it takes nearly three minutes. I've done a very light amount of profiling...
Relevant proposal: https://hal.inria.fr/hal-01806154 This will subsume #35.
The `intros h g k`, `hc : case ...`, etc. forms are not documented in the reference manual.