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

Logic.agda not compiling #13

Closed Agnishom closed 6 years ago

Agnishom commented 6 years ago

I am very new to agda, and I am not sure I am doing it right, but when I try to compile Logic.agda with Ctrl+C and Ctrl+L on emacs, I get the following message:

/home/agnishom/test/Math/Math/Logic.agda:33,5-30
The type of the constructor does not fit in the sort of the
datatype, since Set (.Agda.Primitive.lsuc n) is not less or equal
than Set n
when checking the constructor ∨ᵢᵣ in the declaration of _∨_
Agnishom commented 6 years ago

Sorry, this compiles fine with the latest version of Agda