[Agda] Inspect.

[flicky frans]

Andreas Abel,
>check the standard library with your simplified Reveal

Quick search gave me quite a few test cases in the standard library:
one in Data.List.Any.Properties and two in Data.List.NonEmpty. They
are passed.

>check your own projects and maybe some others you get hold of

I have only a couple test cases. They are passed too. Maybe someone has more?

>submit a pull request to agda/agda-stdlib on github

I can try, but I'm not experienced with github. Maybe someone, who
knows how to submit a pull request, does this instead of me?

Aaron Stump, look at this stackoverflow question:
http://stackoverflow.com/questions/27667359/agda-type-of-proofs-and-with-clause

2014-12-29 17:57 GMT+03:00, Aaron Stump <aaron-stump at uiowa.edu>:
> I'd like to ask a related (I hope) question: what is the paradigmatic
> simple example where inspect fails, but inspect on steroids succeeds?
>
> Thanks,
> Aaron
>
> On 12/29/2014 08:25 AM, Andrés Sicard-Ramírez wrote:
>>
>> On 29 December 2014 at 08:59, Andreas Abel <andreas.abel at ifi.lmu.de
>> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>>
>>     The way to proceed here would be
>>
>>     * check the standard library with your simplified Reveal
>>     * check your own projects and maybe some others you get hold of
>>     * submit a pull request to agda/agda-stdlib on github.
>>
>>
>> ​In the last step, please submit your pull request using the 2.4.2.1
>> branch.
>>
>> --
>> Andrés
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>