aboutsummaryrefslogtreecommitdiff
path: root/mltt/lib/List.thy (unfollow)
Commit message (Collapse)AuthorFilesLines
2021-01-31rename things + some small changesJosh Chen1-0/+0
2021-01-21renamingsJosh Chen1-3/+3
2021-01-18Swapped notation for metas (now ?) and holes (now {}), other notation and ↵Josh Chen1-7/+7
name changes.
2020-08-14(FEAT) Context data slots for known types and conditional type rules, as ↵Josh Chen1-1/+1
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 Chen1-5/+5
behavior
2020-07-31(FEAT) Term elaboration of assumption and goal statements.Josh Chen1-5/+5
. 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-211. Type-checking/inference now more principled, and the implementation is ↵Josh Chen1-6/+7
better. 2. Changed most tactics to context tactics.
2020-07-09Non-annotated object lambdaJosh Chen1-6/+6
2020-07-081. Initial `Definition` keyword. 2. ifelse.Josh Chen1-10/+8
2020-06-15rename foldersJosh Chen1-0/+0
2020-06-031. Type information context dataJosh Chen1-3/+3
2. Small reformulations of rules 3. Bool
2020-06-01reorganize and add some materialJosh Chen1-41/+59
2020-05-31more listJosh Chen1-8/+28
2020-05-28bit more materialJosh Chen1-10/+14
2020-05-28more List and MaybeJosh Chen1-5/+15
2020-05-27change variable name in elim rules and fix small mistakeJosh Chen1-22/+13
2020-05-26Maybe and more ListJosh Chen1-7/+67
2020-05-25notationJosh Chen1-0/+4
2020-05-25Lists + more reorganizingJosh Chen1-0/+79
2020-05-25Reorganize theory structure. In particular, the identity type moves out from ↵Josh Chen1-0/+6
under Spartan to HoTT. Spartan now only has Pi and Sigma.