[Agda] Introducing hypotheses

[Philippe de Rochambeau]

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> 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
> https://lists.chalmers.se/mailman/listinfo/agda

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