[Agda] Introducing hypotheses

[Andreas Nuyts]

Dear Philippe,

These Agda exercise sessions - mostly by Jesper Cockx - may be of 
interest to you:
https://github.com/anuyts/agda-sessions

To answer your question:
tauto₁=\ A B C g f a -> g a (f a)

Best regards,
Andreas

On 18/04/2020 17:32, Philippe de Rochambeau wrote:
> s/« which the user can then apply » /«  letting the use apply them »/
>
>> Le 18 avr. 2020 à 17:30, Philippe de Rochambeau <phiroc at free.fr 
>> <mailto:phiroc at free.fr>> a écrit :
>>
>>
>> Hello,
>>
>> I am attempting to translate a Coq proof into Agda, for learning 
>> purposes (cf. https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf, 
>> p. 9):
>>
>> tauto₁:∀(A B C :Set)→(A →B →C)→(A →B)→A →C
>> tauto₁={ }0
>>
>> Here’s how Coq introduces hypotheses, letting the use apply them.
>>
>> Coq < apply H’.
>> 1 subgoal
>> A : Prop
>> B : Prop
>> C : Prop
>> H : A -> B -> C
>> H’ : A -> B
>> HA : A
>> ============================
>> A
>>
>> How do you do the same thing in Agda?
>>
>> Cheers,
>>
>> Philippe
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200418/60a78675/attachment.html>