aboutsummaryrefslogtreecommitdiff
path: root/Projections.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* working towards biinv_imp_qinvJosh Chen2019-03-261-2/+2
|
* prune import listsJosh Chen2019-03-081-1/+1
|
* Make functions object-levelJosh Chen2019-03-061-21/+19
|
* touchupsJosh Chen2019-02-231-1/+1
|
* Method "quantify" converts product inhabitation into Pure universal ↵Josh Chen2019-02-171-2/+2
| | | | statements. Also misc. cleanups.
* Organize this commit as a backup of the work on type inference done so far; ↵Josh Chen2019-02-111-22/+24
| | | | learnt that I probably need to take a different approach. In particular, should first make the constants completely monomorphic, and then work on full proper type inference, rather than the heuristic approach taken here.
* RenamingJosh Chen2018-09-191-0/+43