The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Set Printing All.

Record C_record := {
 x_record: nat;
 cond_record: x_record = 0
}.

Class C_class := {
 x_class: nat;
 cond_class: x_class = 0
}.

Print C_record.
(*Inductive C_record : Type :=
    Build_C_record : forall x_record : nat, @eq nat x_record O -> C_record

For Build_C_record: Argument scopes are [nat_scope _]*)

Print C_class.
(*Inductive C_class : Type :=
    Build_C_class : forall x_class : nat, @eq nat x_class O -> C_class

For Build_C_class: Argument scopes are [nat_scope _]
*)

About cond_record.
(*cond_record : forall c : C_record, @eq nat (x_record c) O

cond_record is transparent
Expands to: Constant Top.cond_record*)
About cond_class.
(*cond_class : forall C_class : C_class, @eq nat (@x_class C_class) O

Argument C_class is implicit and maximally inserted
cond_class is transparent
Expands to: Constant Top.cond_class
*)

Print cond_record.
(*cond_record =
fun c : C_record =>
match c as c0 return (@eq nat (x_record c0) O) with
| Build_C_record x_record cond_record => cond_record
end
     : forall c : C_record, @eq nat (x_record c) O*)
Print cond_class.
(*cond_class =
fun C_class0 : C_class =>
match C_class0 as C_class return (@eq nat (@x_class C_class) O) with
| Build_C_class x_class cond_class => cond_class
end
     : forall C_class : C_class, @eq nat (@x_class C_class) O

Argument C_class is implicit and maximally inserted*)


Goal forall c, c.(cond_record) = cond_record c.
Proof. reflexivity. Qed.