coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hussain Sobhy <hussain.sob7y AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Examples in Mike Nahas's tutorial
- Date: Wed, 27 Apr 2016 23:08:41 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=hussain.sob7y AT gmail.com; spf=Pass smtp.mailfrom=hussain.sob7y AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f174.google.com
- Ironport-phdr: 9a23:0sA0jBFh2g4zgcXhl1hMmJ1GYnF86YWxBRYc798ds5kLTJ75o8ywAkXT6L1XgUPTWs2DsrQf27qQ4/urADRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nh6bioNaKO01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y48T34NmxtOSzPC5hHrFsPxrzDhv+t7njKdN5LnZb8xUDWmqaxsTUm72288Kzcl/TSP2YRLh6VBrUf5qg==
Hello,
I was going through Mike Nahas's tutorial (https://coq.inria.fr/tutorial-nahas) and I came across two examples which I can't get working on CoqIde.Inductive or (A B:Prop) : Prop := | or_introl : A -> A \/ B | or_intror : B -> A \/ B where "A \/ B" := (or A B) : type_scope.
Theorem left_or : (forall A B : Prop, A -> A \/ B).
Proof.
intros A B.
intros proof_of_A.
pose (proof_of_A_or_B := or_introl proof_of_A : A \/ B).
exact proof_of_A_or_B.
Qed.
In environment
A, B : Prop
proof_of_A : A
The term "proof_of_A" has type "A"
while it is expected to have type
"Prop".
Theorem right_or : (forall A B : Prop, B -> A \/ B).
Proof.
intros A B.
intros proof_of_B.
refine (or_intror _).
exact proof_of_B.
Qed.
In environment
A, B : Prop
proof_of_B : B
The term "or_intror ?P" has type
"forall B0 : Prop, B0 -> ?P \/ B0"
while it is expected to have type
"A \/ B".
- [Coq-Club] Examples in Mike Nahas's tutorial, Hussain Sobhy, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Gabriel Scherer, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Hussain Sobhy, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Hussain Sobhy, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Gabriel Scherer, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Hussain Sobhy, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Gabriel Scherer, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Hussain Sobhy, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Hussain Sobhy, 04/29/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Igor Zhirkov, 04/29/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Gabriel Scherer, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Hussain Sobhy, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Gabriel Scherer, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Hussain Sobhy, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Hussain Sobhy, 04/28/2016
- Re: [Coq-Club] Examples in Mike Nahas's tutorial, Gabriel Scherer, 04/28/2016
Archive powered by MHonArc 2.6.18.