aboutsummaryrefslogtreecommitdiff
path: root/spartan/lib (follow)
Commit message (Collapse)AuthorAgeFilesLines
* (FEAT) Term elaboration of assumption and goal statements.Josh Chen2020-07-313-17/+18
| | | | | | | | | | | | | | | | | | | | . spartan/core/goals.ML . spartan/core/elaboration.ML . spartan/core/elaborated_statement.ML (FEAT) More context tacticals and search tacticals. . spartan/core/context_tactical.ML (FEAT) Improved subgoal focus. Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY). . spartan/core/focus.ML (FIX) Normalize facts in order to be able to resolve properly. . spartan/core/typechecking.ML (MAIN) New definitions. (MAIN) Renamed theories and theorems. (MAIN) Refactor theories to fit new features.
* 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