abella
abella copied to clipboard
abella-prover
An interactive theorem prover based on lambda-tree syntax
Run the following script with Abella in the master branch: ``` Kind pair type -> type -> type. Define map : (A -> B) -> prop by map F. Set...
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...
Implement #121. Summary --- Support Coq-like semi-colons, `try` and `solve` tactics. `induction on 1. intros. case H1; try case H2; search.` Implementation details --- The implementation patches `sequent` by adding...
This PR implements the feature requested by #133. I refer to the original feature request and comment on my modifications: The command added to Abella is `Reprove`, since most of...
Grammar: --- ``` applys [to] [with X1 = T1, ..., Xn = Tn]. applys [with X1 = T1, ..., Xn = Tn]. ``` Why not `apply` --- A script like...
We can write ill-typed code which Abella accepts by using a polymorphic type constructor. Some definitions to provide types to demonstrate the issue: ``` Kind aty type. Type a aty....
Consider the following simplified testcase: ``` Kind t type. Type abs t -> t. Theorem foo : forall (T : t -> t) U V, T U = T V...
Given that one of the possible witnesses is `unfold(id,n,witness1,...,witnessn)` (where the second `n` should really be `k`), wouldn't it make sense to have a tactic `unfold id n`, so that...
Metadata
Owner
Metadata
An interactive theorem prover based on lambda-tree syntax