aboutsummaryrefslogtreecommitdiff
path: root/hott (unfollow)
Commit message (Collapse)AuthorFilesLines
2021-06-28begin refactoring EquivalenceJosh Chen1-0/+458
2021-06-24Bad practice huge commit:Josh Chen5-16/+60
1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file
2021-04-17Patch proof. Now works on Isabelle2021.Josh Chen1-1/+1
2021-04-10start hprop stuffJosh Chen2-0/+27
2021-01-31rename things + some small changesJosh Chen3-45/+38
2021-01-21renamingsJosh Chen3-113/+105
2021-01-18Swapped notation for metas (now ?) and holes (now {}), other notation and ↵Josh Chen4-69/+76
name changes.
2020-09-23Basic experiments adding reduction to the type checkerJosh Chen3-73/+26
2020-08-14(FEAT) Context data slots for known types and conditional type rules, as ↵Josh Chen3-48/+47
well as a separate one for judgmental equality rules. (REF) Goal statement assumptions are now put into the new context data slots. (FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data. (REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context. MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`. (REF) Fixed incompatibilities in theories.
2020-08-09(FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* ↵Josh Chen1-7/+6
goals; resolving with conditional typing judgments (e.g. type family assumptions) is part of check_infer_step
2020-08-051. fix intros method. 2. Couple extra lemmas; good small test cases for ↵Josh Chen2-1/+60
normalization in typechecking/elaboration.
2020-08-03(FEAT) SIDE_CONDS tactical has additional argument specifying how many ↵Josh Chen2-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.
2020-08-02rename some theoremsJosh Chen1-9/+9
2020-07-31(REF) Tweak attribute names in preparation for new logical introduction rule ↵Josh Chen3-21/+21
behavior
2020-07-31(FEAT) Term elaboration of assumption and goal statements.Josh Chen5-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.
2020-07-27Hook elaboration into assumptions mechanismJosh Chen2-50/+55
2020-07-211. Bugfix: implicits now properly name schematic variables. Fixes problems ↵Josh Chen2-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.
2020-07-211. Type-checking/inference now more principled, and the implementation is ↵Josh Chen5-117/+109
better. 2. Changed most tactics to context tactics.
2020-07-09Non-annotated object lambdaJosh Chen4-16/+16
2020-07-08minorJosh Chen2-3/+3
2020-06-19reorganizeJosh Chen1-0/+43
2020-06-03rule nameJosh Chen1-1/+1
2020-06-01reorganize and add some materialJosh Chen1-3/+3
2020-05-31multiplicationJosh Chen1-6/+72
2020-05-31transport methodJosh Chen1-0/+2
2020-05-30add and mul recurse on second argument instead of firstJosh Chen1-20/+49
2020-05-30fix nameJosh Chen1-1/+5
2020-05-29proved a few oopses + minor tweaksJosh Chen2-30/+23
2020-05-29clean up Eckmann-Hilton and move to IdentityJosh Chen3-209/+206
2020-05-29minorJosh Chen1-1/+1
2020-05-27change variable name in elim rules and fix small mistakeJosh Chen1-7/+7
2020-05-27minorJosh Chen2-8/+3
2020-05-271. Define Maybe in terms of other types. 2. Move More_Types to SpartanJosh Chen1-91/+0
2020-05-27Eckmann-Hilton, first passJosh Chen2-3/+192
2020-05-26new materialJosh Chen5-34/+58
2020-05-25more reorganizingJosh Chen4-12/+10
2020-05-25Lists + more reorganizingJosh Chen4-12/+14
2020-05-25Reorganize theory structure. In particular, the identity type moves out from ↵Josh Chen3-1/+881
under Spartan to HoTT. Spartan now only has Pi and Sigma.
2020-05-25minorJosh Chen1-1/+1
2020-05-25some arithmeticJosh Chen1-17/+30
2020-05-24new work on elimination tacticJosh Chen1-1/+1
2020-05-22some tweaks and comments, in preparation for general inductive type eliminationJosh Chen1-4/+47
2020-04-16minor namingJosh Chen1-9/+13
2020-04-031. change var names. 2. add and mulJosh Chen1-8/+11
2020-04-031. Base theory. 2. Fix Nat axioms, addition.Josh Chen2-11/+21
2020-04-02Brand-spanking new version using Spartan infrastructureJosh Chen2-0/+141
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-29 12:53:17 +0000