| Commit message (Collapse) | Author | Files | Lines | ||
|---|---|---|---|---|---|
| 2022-06-29 | (broken) update hott for Isabelle 2021-1HEADmaster | stuebinm | 1 | -11/+12 | |
| this just replaces all instance of `this` with instances of `infer`. Unfortunately, it looks likes something else also broke, and I have no idea what it is (but the proof for equiv_if_equal fails). Sadly this means we can't get to univalence for now … (but rn I'm too tired to try anything else with it) | |||||
| 2021-06-24 | Bad practice huge commit: | Josh Chen | 1 | -3/+3 | |
| 1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file | |||||
| 2021-04-17 | Patch proof. Now works on Isabelle2021. | Josh Chen | 1 | -1/+1 | |
| 2021-01-31 | rename things + some small changes | Josh Chen | 1 | -42/+35 | |
| 2021-01-21 | renamings | Josh Chen | 1 | -50/+50 | |
| 2021-01-18 | Swapped notation for metas (now ?) and holes (now {}), other notation and ↵ | Josh Chen | 1 | -46/+46 | |
| name changes. | |||||
| 2020-09-23 | Basic experiments adding reduction to the type checker | Josh Chen | 1 | -29/+18 | |
| 2020-08-14 | (FEAT) Context data slots for known types and conditional type rules, as ↵ | Josh Chen | 1 | -22/+25 | |
| 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-05 | 1. fix intros method. 2. Couple extra lemmas; good small test cases for ↵ | Josh Chen | 1 | -0/+40 | |
| normalization in typechecking/elaboration. | |||||
| 2020-08-03 | (FEAT) SIDE_CONDS tactical has additional argument specifying how many ↵ | Josh Chen | 1 | -1/+1 | |
| 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-07-31 | (REF) Tweak attribute names in preparation for new logical introduction rule ↵ | Josh Chen | 1 | -2/+2 | |
| behavior | |||||
| 2020-07-31 | (FEAT) Term elaboration of assumption and goal statements. | Josh Chen | 1 | -120/+119 | |
| . 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-27 | Hook elaboration into assumptions mechanism | Josh Chen | 1 | -40/+42 | |
| 2020-07-21 | 1. Bugfix: implicits now properly name schematic variables. Fixes problems ↵ | Josh Chen | 1 | -7/+10 | |
| 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-21 | 1. Type-checking/inference now more principled, and the implementation is ↵ | Josh Chen | 1 | -78/+69 | |
| better. 2. Changed most tactics to context tactics. | |||||
| 2020-07-09 | Non-annotated object lambda | Josh Chen | 1 | -4/+4 | |
| 2020-07-08 | minor | Josh Chen | 1 | -2/+2 | |
| 2020-06-01 | reorganize and add some material | Josh Chen | 1 | -3/+3 | |
| 2020-05-31 | transport method | Josh Chen | 1 | -0/+2 | |
| 2020-05-29 | clean up Eckmann-Hilton and move to Identity | Josh Chen | 1 | -0/+181 | |
| 2020-05-27 | minor | Josh Chen | 1 | -0/+1 | |
| 2020-05-27 | Eckmann-Hilton, first pass | Josh Chen | 1 | -0/+16 | |
| 2020-05-26 | new material | Josh Chen | 1 | -23/+5 | |
| 2020-05-25 | Lists + more reorganizing | Josh Chen | 1 | -2/+2 | |
| 2020-05-25 | Reorganize theory structure. In particular, the identity type moves out from ↵ | Josh Chen | 1 | -0/+0 | |
| under Spartan to HoTT. Spartan now only has Pi and Sigma. | |||||
| 2020-05-25 | slightly nicer homotopy proofs with calculations | Josh Chen | 1 | -1/+2 | |
| 2020-05-25 | use existing calculation infrastructure for sym and trans | Josh Chen | 1 | -12/+3 | |
| 2020-05-25 | 1. equality method now uses general elimination tactic. 2. New constant `` ↵ | Josh Chen | 1 | -51/+89 | |
| refers to rhs of equalities. | |||||
| 2020-05-24 | new work on elimination tactic | Josh Chen | 1 | -1/+1 | |
| 2020-05-22 | some tweaks and comments, in preparation for general inductive type elimination | Josh Chen | 1 | -6/+7 | |
| 2020-04-02 | 1. make id function an abbrev. 2. fix reduce method | Josh Chen | 1 | -1/+1 | |
| 2020-04-02 | Brand-spanking new version using Spartan infrastructure | Josh Chen | 1 | -0/+433 | |
 |
index : Isabelle-HoTT | |
| trying to make Isabelle/HoTT work with Isabelle 2021-1 |
| aboutsummaryrefslogtreecommitdiff |