[Agda] Introducing hypotheses

[Philippe de Rochambeau]

Very enlightening.

Thank you, Andreas.

> Le 18 avr. 2020 à 17:37, Andreas Nuyts <andreas.nuyts at kuleuven.be> a écrit :
> 
> Dear Philippe,
> 
> These Agda exercise sessions - mostly by Jesper Cockx - may be of interest to you:
> https://github.com/anuyts/agda-sessions <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 <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 <https://lists.chalmers.se/mailman/listinfo/agda>
>> 
>> 
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>
> 

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