[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