search

berenoguz / Math

Formalization of Mathematics using Type Theory of Agda Programming Language
GNU General Public License v3.0
11 stars 0 forks source link

Stronger inference #7

Closed berenoguz closed 6 years ago

berenoguz commented 6 years ago

Fix unnecessary ∀ symbols and add them where necessary. Sometimes you don't need to give instances as inputs and Agda can infer them.

berenoguz commented 6 years ago

Shouls be done. I might reopen this.