[Agda] `let' and `case'

Sergei Meshveliani mechvel at botik.ru
Sat Apr 9 21:05:55 CEST 2016


Dear Agda developers,

I have an impression that treating of  `let' and case_of_  has changed,
and is now much better than 1-2 years ago.
In old days I almost stopped using case_of_ and `let', because the type
checker reported errors, so I used `with' almost everywhere.
For example, I was stuck when one of the `case' branches returned
\bot-elim (there was needed a certain subtle version of `case').

Since March 2016, I return trying case_of_ and `let', and find that they
work everywhere. 

I do not provide concrete examples, this is an impression.
But has the type checker changed essentially with this respect?

Regards,

------
Sergei 



More information about the Agda mailing list