diff options
| author | Gaëtan Gilbert | 2018-11-02 14:08:54 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 14:08:54 +0100 |
| commit | 3f22c11c650b6ef7cc0770418255865ebdbfb1ae (patch) | |
| tree | 2324c16061364deb0c2d2231a804f66b619ddc9a /dev/ci | |
| parent | 9b0a4b002e324d523b01e17fba7ba631a651f6b0 (diff) | |
Expose Typing.judge_of_apply
This can be useful to avoid [Typing.type_of (App (f,args))] when
working with universe polymorphism.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions