The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

A type class with one field and no curly braces is implemented via a simple alias definition.  So, to give a silly example:

Class Commutative {A:Type} (op : A -> A -> A) : Prop :=

commutativity : forall x y:A, op x y = op y x.

Lemma silly : Commutative Peano.minus -> False.

Proof.

intros.

red in H.  (* or unfold Commutative in H. *)

discriminate (H 0 1).

Qed.

Class Commutative' {A:Type} (op : A -> A -> A) : Prop := {

  commutativity' : forall x y:A, op x y = op y x

}.

Lemma silly' : Commutative' Peano.minus -> False.

Proof.

intros.

destruct H.

discriminate (commutativity'0 0 1).

Qed.

-- 

Daniel Schepler

On Thu, Jan 30, 2014 at 12:09 PM, Richard Dapoigny <richard.dapoigny AT univ-savoie.fr> wrote:

Hi everybody,
While "destruct" works fine with type classes having multiple fields I do not succeed to get the field if there is only a single field.
Does anyone knows some tactic to extract the field in an operational type class?
Thanks in advance,
Rich.

--

Attachment: Sign.jpg
Description: JPEG image