CODEWITHSUNDEEP
coq
Bob
Bob

Reputation: 1743

Not pretty-printing a field of a record

Suppose I have such record type:

Record myRec : Type := {
  myNat : nat;
  myProof : myNat > 0
}.

How can I tell Coq to parse but not pretty-print (i.e., hide) the field myProof of a value of type myRec?

Can it be set while declaring the record type?

Or should it be done using the Notation command and the only printing syntax modifier?

Upvotes: 2

Views: 142

Answers (1)

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

The way I would do it is indeed with notations.

Record myRec : Type := myRecBuild {
  myNat : nat ;
  myProof : myNat > 0
}.

Notation "⟪ x ⟫" := (myRecBuild x _).

Now if you have a value of myRec it will only print the relevant part.

Lemma foo :
  forall (x y : myRec),
    x.(myNat) = y.(myNat) ->
    x = x.
Proof.
  intros [x hx] [y hy] e.
  simpl in e. (* replaces myNat ⟪ x ⟫ with x *)
  (* Goal is now ⟪ x ⟫ = ⟪ x ⟫, hiding hx and hy *)
Abort.

I would argue that you don't need the only printing option. In fact, this can be handy if you want to easily provide the relevant part and leave the rest to automation / tactics.

Lemma bar :
  exists (x : myRec), x.(myNat) = 1.
Proof.
  unshelve eexists ⟪ 1 ⟫.
  - auto.
  - reflexivity.
Qed.

This can become particularly handy when using Program or Equations.

Upvotes: 1

Related Questions