aboutsummaryrefslogtreecommitdiff
path: root/spartan/lib (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 1. Type-checking/inference now more principled, and the implementation is ↵Josh Chen2020-07-213-22/+28
| | | | better. 2. Changed most tactics to context tactics.
* Non-annotated object lambdaJosh Chen2020-07-093-20/+17
|
* 1. Initial `Definition` keyword. 2. ifelse.Josh Chen2020-07-083-15/+55
|
* rename foldersJosh Chen2020-06-153-0/+372
|
* Reorganize theory structure. In particular, the identity type moves out from ↵Josh Chen2020-05-2510-1846/+0
| | | | under Spartan to HoTT. Spartan now only has Pi and Sigma.
* new elimination tacticJosh Chen2020-05-251-17/+65
|
* new work on elimination tacticJosh Chen2020-05-242-34/+85
|
* small commentJosh Chen2020-05-241-0/+2
|
* some tweaks and comments, in preparation for general inductive type eliminationJosh Chen2020-05-223-3/+7
|
* update for Isabelle2020Josh Chen2020-04-162-2/+2
|
* Brand-spanking new version using Spartan infrastructureJosh Chen2020-04-0210-0/+1741