[Agda] I want implicit coercions in Agda

[Thorsten Altenkirch]

I meant every group is a monoid...

On 19/11/2018, 09:01, "Agda on behalf of Thorsten Altenkirch"
<agda-bounces at lists.chalmers.se on behalf of
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

>Another source of coercions are surjections from record subtyping, e.g.
>every monoid is a group etc.
>
>On 19/11/2018, 04:44, "Agda on behalf of Peter Hancock"
><agda-bounces at lists.chalmers.se on behalf of hancock at fastmail.fm> wrote:
>
>>I presume coercions are injective functions that resolve type-clashes
>>between 
>>things like natural numbers and signed integers, or fractions, etc.
>>There are times when we want to see these things, and there are times
>>when we would like them to be hidden.
>>Could one have a "pedantry" knob when editing or browsing agda?
>>At pedantry level 11 absolutely nothing would be hidden....
>>
>
>
>
>
>This message and any attachment are intended solely for the addressee
>and may contain confidential information. If you have received this
>message in error, please contact the sender and delete the email and
>attachment. 
>
>Any views or opinions expressed by the author of this email do not
>necessarily reflect the views of the University of Nottingham. Email
>communications with the University of Nottingham may be monitored
>where permitted by law.
>
>
>
>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.