thibautbenjamin / catt

Coherence typechecker for infinity categories
MIT License
18 stars 2 forks source link

Feature/first class application #84

Open thibautbenjamin opened 3 weeks ago

thibautbenjamin commented 3 weeks ago

Add first class term applications to the kernel to reduce the number of times substitution applications are computed