aboutsummaryrefslogtreecommitdiff
path: root/hott (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 1. fix intros method. 2. Couple extra lemmas; good small test cases for ↵Josh Chen2020-08-052-1/+60
| | | | normalization in typechecking/elaboration.
* (FEAT) SIDE_CONDS tactical has additional argument specifying how many ↵Josh Chen2020-08-032-15/+7
| | | | | | | | initial subgoals to skip applying the side condition solver to. (FEAT) `intro`, `intros` methods for "logical introduction rules" (as opposed to typechecking `intr` attribute), only works on conclusions with rigid type. (FEAT) CREPEAT_N bounded repetition tactical, used in `intros n` method.
* rename some theoremsJosh Chen2020-08-021-9/+9
|
* (REF) Tweak attribute names in preparation for new logical introduction rule ↵Josh Chen2020-07-313-21/+21
| | | | behavior
* (FEAT) Term elaboration of assumption and goal statements.Josh Chen2020-07-315-402/+400
| | | | | | | | | | | | | | | | | | | | . 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.
* Hook elaboration into assumptions mechanismJosh Chen2020-07-272-50/+55
|
* 1. Bugfix: implicits now properly name schematic variables. Fixes problems ↵Josh Chen2020-07-212-19/+22
| | | | caused by variable name clashes. 2. reduce method now more principled: restricts to repeating on first subgoal. 3. An example declarative proof in Equivalence.thy.
* 1. Type-checking/inference now more principled, and the implementation is ↵Josh Chen2020-07-215-117/+109
| | | | better. 2. Changed most tactics to context tactics.
* Non-annotated object lambdaJosh Chen2020-07-094-16/+16
|
* minorJosh Chen2020-07-082-3/+3
|
* reorganizeJosh Chen2020-06-191-0/+43
|
* rule nameJosh Chen2020-06-031-1/+1
|
* reorganize and add some materialJosh Chen2020-06-011-3/+3
|
* multiplicationJosh Chen2020-05-311-6/+72
|
* transport methodJosh Chen2020-05-311-0/+2
|
* add and mul recurse on second argument instead of firstJosh Chen2020-05-301-20/+49
|
* fix nameJosh Chen2020-05-301-1/+5
|
* proved a few oopses + minor tweaksJosh Chen2020-05-292-30/+23
|
* clean up Eckmann-Hilton and move to IdentityJosh Chen2020-05-293-209/+206
|
* minorJosh Chen2020-05-291-1/+1
|
* change variable name in elim rules and fix small mistakeJosh Chen2020-05-271-7/+7
|
* minorJosh Chen2020-05-272-8/+3
|
* 1. Define Maybe in terms of other types. 2. Move More_Types to SpartanJosh Chen2020-05-271-91/+0
|
* Eckmann-Hilton, first passJosh Chen2020-05-272-3/+192
|
* new materialJosh Chen2020-05-265-34/+58
|
* more reorganizingJosh Chen2020-05-254-12/+10
|
* Lists + more reorganizingJosh Chen2020-05-254-12/+14
|
* Reorganize theory structure. In particular, the identity type moves out from ↵Josh Chen2020-05-253-1/+881
| | | | under Spartan to HoTT. Spartan now only has Pi and Sigma.
* minorJosh Chen2020-05-251-1/+1
|
* some arithmeticJosh Chen2020-05-251-17/+30
|
* new work on elimination tacticJosh Chen2020-05-241-1/+1
|
* some tweaks and comments, in preparation for general inductive type eliminationJosh Chen2020-05-221-4/+47
|
* minor namingJosh Chen2020-04-161-9/+13
|
* 1. change var names. 2. add and mulJosh Chen2020-04-031-8/+11
|
* 1. Base theory. 2. Fix Nat axioms, addition.Josh Chen2020-04-032-11/+21
|
* Brand-spanking new version using Spartan infrastructureJosh Chen2020-04-022-0/+141
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 22:04:01 +0000