coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Nadeem Abdul Hamid <nadeem AT acm.org>
- To: Robert Rothenberg <robrwo AT gmail.com>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Higher-order logic
- Date: Mon, 16 Feb 2009 09:43:54 -0500
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:cc:message-id:from:to:in-reply-to:content-type :content-transfer-encoding:mime-version:subject:date:references :x-mailer; b=jH1X9PJsGE3sd4ImqSEB+j73Pr60MnuxiD0I02caVOzUHaRPYzLD7ljUv2ou72QyOA IjuNfMh9P7aacWE8eBAaXY+/3n251dHNyG90fzwCjpoUAPWAbBaExq7BTne7BMENApyX h0Jcmalxu5IOXBnDyOxX5pfh5Rd2YI9HFcJ/U=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Do you mean like this?
Check (fun (x y : Set) => forall P : Set -> Prop, P x -> P y).
Definition myrelation : Set -> Set -> Prop :=
fun x y => forall P : Set -> Prop, P x -> P y.
On Feb 16, 2009, at 9:32 AM, Robert Rothenberg wrote:
Given predicates Set->Prop, how do I define a relation Set->Set->Prop
of something like
forall P:Set->Prop. P x -> P y ?
- [Coq-Club] Higher-order logic, Robert Rothenberg
- Re: [Coq-Club] Higher-order logic, Nadeem Abdul Hamid
Archive powered by MhonArc 2.6.16.