aboutsummaryrefslogtreecommitdiff
path: root/hott (follow)
Commit message (Expand)AuthorAgeFilesLines
* (broken) update hott for Isabelle 2021-1HEADmasterstuebinm2022-06-293-23/+24
* 1. Thm/def statement display. 2. Syntax + computation proof.Josh Chen2021-06-281-2/+2
* begin refactoring EquivalenceJosh Chen2021-06-281-0/+458
* Bad practice huge commit:Josh Chen2021-06-245-16/+60
* Patch proof. Now works on Isabelle2021.Josh Chen2021-04-171-1/+1
* start hprop stuffJosh Chen2021-04-102-0/+27
* rename things + some small changesJosh Chen2021-01-313-45/+38
* renamingsJosh Chen2021-01-213-113/+105
* Swapped notation for metas (now ?) and holes (now {}), other notation and nam...Josh Chen2021-01-184-69/+76
* Basic experiments adding reduction to the type checkerJosh Chen2020-09-233-73/+26
* (FEAT) Context data slots for known types and conditional type rules, as well...Josh Chen2020-08-143-48/+47
* (FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* go...Josh Chen2020-08-091-7/+6
* 1. fix intros method. 2. Couple extra lemmas; good small test cases for norma...Josh Chen2020-08-052-1/+60
* (FEAT) SIDE_CONDS tactical has additional argument specifying how many initia...Josh Chen2020-08-032-15/+7
* 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
* (FEAT) Term elaboration of assumption and goal statements.Josh Chen2020-07-315-402/+400
* Hook elaboration into assumptions mechanismJosh Chen2020-07-272-50/+55
* 1. Bugfix: implicits now properly name schematic variables. Fixes problems ca...Josh Chen2020-07-212-19/+22
* 1. Type-checking/inference now more principled, and the implementation is bet...Josh Chen2020-07-215-117/+109
* 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
* 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 04:50:17 +0000