| Commit message (Collapse) | Author | Files | Lines | ||
|---|---|---|---|---|---|
| 2021-06-24 | Bad practice huge commit: | Josh Chen | 1 | -1/+1 | |
| 1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file | |||||
| 2021-01-31 | rename things + some small changes | Josh Chen | 1 | -1/+3 | |
| 2021-01-21 | renamings | Josh Chen | 1 | -3/+3 | |
| 2021-01-18 | Swapped notation for metas (now ?) and holes (now {}), other notation and ↵ | Josh Chen | 1 | -1/+1 | |
| name changes. | |||||
| 2020-08-14 | (FEAT) Context data slots for known types and conditional type rules, as ↵ | Josh Chen | 1 | -1/+2 | |
| 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-07-31 | (REF) Tweak attribute names in preparation for new logical introduction rule ↵ | Josh Chen | 1 | -4/+4 | |
| behavior | |||||
| 2020-07-31 | (FEAT) Term elaboration of assumption and goal statements. | Josh Chen | 1 | -3/+3 | |
| . 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-21 | 1. Type-checking/inference now more principled, and the implementation is ↵ | Josh Chen | 1 | -13/+17 | |
| better. 2. Changed most tactics to context tactics. | |||||
| 2020-07-09 | Non-annotated object lambda | Josh Chen | 1 | -6/+6 | |
| 2020-07-08 | 1. Initial `Definition` keyword. 2. ifelse. | Josh Chen | 1 | -4/+46 | |
| 2020-06-15 | rename folders | Josh Chen | 1 | -0/+0 | |
| 2020-06-03 | 1. Type information context data | Josh Chen | 1 | -0/+8 | |
| 2. Small reformulations of rules 3. Bool | |||||
| 2020-05-28 | more List and Maybe | Josh Chen | 1 | -0/+3 | |
| 2020-05-27 | change variable name in elim rules and fix small mistake | Josh Chen | 1 | -1/+2 | |
| 2020-05-27 | 1. Define Maybe in terms of other types. 2. Move More_Types to Spartan | Josh Chen | 1 | -2/+3 | |
| 2020-05-25 | more reorganizing | Josh Chen | 1 | -1/+1 | |
| 2020-05-25 | Lists + more reorganizing | Josh Chen | 1 | -9/+1 | |
| 2020-05-25 | Reorganize theory structure. In particular, the identity type moves out from ↵ | Josh Chen | 1 | -1/+1 | |
| under Spartan to HoTT. Spartan now only has Pi and Sigma. | |||||
| 2020-04-03 | 1. Base theory. 2. Fix Nat axioms, addition. | Josh Chen | 1 | -2/+11 | |
| 2020-04-02 | Brand-spanking new version using Spartan infrastructure | Josh Chen | 1 | -0/+90 | |
 |
index : Isabelle-HoTT | |
| trying to make Isabelle/HoTT work with Isabelle 2021-1 |
| aboutsummaryrefslogtreecommitdiff |