aboutsummaryrefslogtreecommitdiff
path: root/spartan/lib (unfollow)
Commit message (Expand)AuthorFilesLines
2020-07-31(REF) Tweak attribute names in preparation for new logical introduction rule ...Josh Chen3-10/+10
2020-07-31(FEAT) Term elaboration of assumption and goal statements.Josh Chen3-17/+18
2020-07-211. Type-checking/inference now more principled, and the implementation is bet...Josh Chen3-22/+28
2020-07-09Non-annotated object lambdaJosh Chen3-20/+17
2020-07-081. Initial `Definition` keyword. 2. ifelse.Josh Chen3-15/+55
2020-06-15rename foldersJosh Chen3-0/+372
2020-05-25Reorganize theory structure. In particular, the identity type moves out from ...Josh Chen10-1846/+0
2020-05-25new elimination tacticJosh Chen1-17/+65
2020-05-24new work on elimination tacticJosh Chen2-34/+85
2020-05-24small commentJosh Chen1-0/+2
2020-05-22some tweaks and comments, in preparation for general inductive type eliminationJosh Chen3-3/+7
2020-04-16update for Isabelle2020Josh Chen2-2/+2
2020-04-02Brand-spanking new version using Spartan infrastructureJosh Chen10-0/+1741
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-18 08:06:59 +0000