Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | Merge branch '2019': beginning type inference automation. | Josh Chen | 2019-02-05 | 5 | -122/+226 | |
|\ | ||||||
| * | Add cong named theorem for congruence rules | Josh Chen | 2019-02-05 | 2 | -5/+9 | |
| | | ||||||
| * | Basic type inference for composed lambda terms! | Josh Chen | 2019-02-05 | 1 | -18/+11 | |
| | | ||||||
| * | Decided to keep terms eta-expanded | Josh Chen | 2019-02-05 | 1 | -0/+2 | |
| | | ||||||
| * | Type inference setup begun - first use-case for function composition. | Josh Chen | 2019-02-05 | 3 | -61/+118 | |
| | | ||||||
| * | 1. Change syntax to rely less on unicode/control symbols. | Josh Chen | 2019-02-04 | 3 | -53/+116 | |
| | | | | | | | | 2. Begin work on object-level type inference and input syntax help. | |||||
| * | Text remarks | Josh Chen | 2019-01-31 | 1 | -3/+7 | |
| | | ||||||
| * | Clean and comment methods file | Josh Chen | 2019-01-30 | 1 | -41/+34 | |
| | | ||||||
| * | Remove "constrained" notation for type families. Clean and document. | Josh Chen | 2019-01-30 | 1 | -20/+13 | |
| | | ||||||
| * | Begin refactor | Josh Chen | 2019-01-30 | 1 | -12/+7 | |
| | | ||||||
* | | Update README.md | Josh Chen | 2018-09-20 | 1 | -1/+1 | |
|/ | | | Remove DOI badge | |||||
* | Derive can prove pathcomp_comp. Fix typo. | Josh Chen | 2018-09-20 | 2 | -16/+2 | |
| | ||||||
* | Application should bind tighter than composition | Josh Chen | 2018-09-20 | 2 | -3/+3 | |
| | ||||||
* | Rename properties of equality + more properties. Output formatting for ` | Josh Chen | 2018-09-20 | 2 | -1/+216 | |
| | ||||||
* | Renaming | Josh Chen | 2018-09-19 | 2 | -220/+0 | |
| | ||||||
* | Renaming | Josh Chen | 2018-09-19 | 3 | -3/+46 | |
| | ||||||
* | Not sure what advantage is provided by having eta-expanded forms in the ↵ | Josh Chen | 2018-09-19 | 5 | -12/+12 | |
| | | | | rules. Removing for now. | |||||
* | proof of associativity of path composition | Josh Chen | 2018-09-19 | 2 | -27/+73 | |
| | ||||||
* | Merge branch 'larsrh-topic/root' | Josh Chen | 2018-09-18 | 4 | -2/+27 | |
|\ | ||||||
| * | Add ROOT. No eta-contraction | Josh Chen | 2018-09-18 | 2 | -2/+18 | |
| | | ||||||
| * | add ROOT file | Lars Hupel | 2018-09-18 | 3 | -2/+11 | |
|/ | ||||||
* | Load Univalence by default | Josh Chen | 2018-09-18 | 1 | -0/+1 | |
| | ||||||
* | Update README.md | Josh Chen | 2018-09-18 | 1 | -0/+6 | |
| | ||||||
* | Update README.md | Josh Chen | 2018-09-18 | 1 | -16/+0 | |
| | ||||||
* | Merge branch 'develop', ready for release 0.1.0 | Josh Chen | 2018-09-18 | 19 | -1088/+588 | |
|\ | ||||||
| * | Overhaul of the theory presentations. New methods in HoTT_Methods.thy for ↵ | Josh Chen | 2018-09-18 | 15 | -273/+177 | |
| | | | | | | | | handling universes. Commit for release 0.1.0! | |||||
| * | Theories fully reorganized. Well-formedness rules removed. New methods etc. | Josh Chen | 2018-09-18 | 6 | -471/+158 | |
| | | ||||||
| * | Clean up Equal.thy + some other tweaks | Josh Chen | 2018-09-17 | 3 | -40/+28 | |
| | | ||||||
| * | Tweak proof | Josh Chen | 2018-09-17 | 2 | -10/+7 | |
| | | ||||||
| * | Reorganizing theories | Josh Chen | 2018-09-17 | 9 | -219/+155 | |
| | | ||||||
| * | Moved function composition lemmas into Prod.thy | Josh Chen | 2018-09-17 | 2 | -108/+51 | |
| | | ||||||
| * | Reorganized HoTT_Base, updated theories | Josh Chen | 2018-09-16 | 16 | -207/+635 | |
| |\ | ||||||
| * | | begin reorganizing | Josh Chen | 2018-09-15 | 2 | -10/+11 | |
| | | | ||||||
| * | | Trying to atomize universal quantification | Josh Chen | 2018-08-19 | 1 | -0/+9 | |
| | | | ||||||
| * | | Higher groupoid structure of types | Josh Chen | 2018-08-19 | 1 | -4/+67 | |
| | | | ||||||
* | | | Update README.md | Josh Chen | 2018-09-17 | 1 | -3/+1 | |
| | | | ||||||
* | | | Update README.md | Josh Chen | 2018-09-12 | 1 | -2/+2 | |
| | | | ||||||
* | | | Update README.md | Josh Chen | 2018-09-12 | 1 | -1/+1 | |
| | | | ||||||
* | | | Add DOI badge | Josh Chen | 2018-09-12 | 1 | -0/+2 | |
| |/ |/| | ||||||
* | | Final commit before first release | Josh Chen | 2018-09-12 | 1 | -1/+1 | |
| | | ||||||
* | | Merge branch 'master' of github.com:jaycech3n/Isabelle-HoTT | Josh Chen | 2018-09-12 | 1 | -3/+7 | |
|\ \ | ||||||
| * | | Update README.md | Josh Chen | 2018-09-11 | 1 | -3/+7 | |
| | | | ||||||
* | | | Some final touchups before release 0.1 for the MS thesis | Josh Chen | 2018-09-12 | 6 | -7/+9 | |
|/ / | ||||||
* | | Add the univalence axiom | Josh Chen | 2018-09-11 | 3 | -4/+71 | |
| | | ||||||
* | | Running into trouble with the polymorphic identity function | Josh Chen | 2018-09-11 | 3 | -17/+80 | |
| | | ||||||
* | | Implementing univalence | Josh Chen | 2018-09-11 | 3 | -0/+81 | |
| | | ||||||
* | | Go back to higher-order application notation | Josh Chen | 2018-09-11 | 11 | -139/+138 | |
| | | ||||||
* | | Merge branch 'master' of github.com:jaycech3n/Isabelle-HoTT | Josh Chen | 2018-08-30 | 1 | -1/+1 | |
|\ \ | ||||||
| * | | Update README.md | Josh Chen | 2018-08-30 | 1 | -1/+1 | |
| | | | ||||||
* | | | Some higher groupoid structure proofs | Josh Chen | 2018-08-30 | 2 | -2/+56 | |
|/ / |