aboutsummaryrefslogtreecommitdiff
path: root/ROOT (follow)
Commit message (Collapse)AuthorAgeFilesLines
* clean up Eckmann-Hilton and move to IdentityJosh Chen2020-05-291-1/+0
|
* reorganize folder structureJosh Chen2020-05-281-4/+3
|
* move More_Types to SpartanJosh Chen2020-05-271-1/+1
|
* Eckmann-Hilton, first passJosh Chen2020-05-271-0/+1
|
* add MaybeJosh Chen2020-05-261-0/+1
|
* more reorganizingJosh Chen2020-05-251-3/+2
|
* Lists + more reorganizingJosh Chen2020-05-251-2/+3
|
* Reorganize theory structure. In particular, the identity type moves out from ↵Josh Chen2020-05-251-4/+14
| | | | under Spartan to HoTT. Spartan now only has Pi and Sigma.
* update for Isabelle2020Josh Chen2020-04-161-0/+1
|
* fix ROOTJosh Chen2020-04-031-1/+1
|
* Brand-spanking new version using Spartan infrastructureJosh Chen2020-04-021-22/+21
|
* 1. Change syntax to rely less on unicode/control symbols.Josh Chen2019-02-041-1/+2
| | | | 2. Begin work on object-level type inference and input syntax help.
* Add ROOT. No eta-contractionJosh Chen2018-09-181-2/+16
|
* add ROOT fileLars Hupel2018-09-181-0/+10