aboutsummaryrefslogtreecommitdiff
path: root/typing.ML (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Explicit references in antiquotations in typing.ML. Move trace switch ↵Josh Chen2019-02-101-6/+3
| | | | definition to HoTT_Base.
* Type information storage functionality (assume_type, assume_types keywords) ↵Josh Chen2019-02-101-38/+167
| | | | done! Inference and pretty-printing for function composition done.
* Type inference setup begun - first use-case for function composition.Josh Chen2019-02-051-0/+91