[Agda] repeated Level.suc

Sergei Meshveliani mechvel at botik.ru
Fri Aug 30 15:18:50 CEST 2013

Dear Agda developers,

When the  level  does not fit, the checker  
(in Agda of darcs August 2013)

reports of level expressions like 
                                  suc l' ⊔ (suc l ⊔ suc c)          (e)

Probably it is better to simplify such expressions. 
For example,
             (e) -->  suc (l' ⊔ l ⊔ c)



More information about the Agda mailing list