Coercions used when printing themselves · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: Coercions used when printing themselves

Janno (Jun 12 2020 at 23:21):

Is this a known printing bug?

From stdpp Require Import telescopes.
Print tele.
(* Inductive tele@{stdpp.telescopes.5} : Type :=  TeleO : tele | TeleS : forall X : Type, (X -> tele) -> tele *)
Print tele_arg.
(*
Inductive tele_arg@{stdpp.telescopes.39} : tele -> Type :=
    TargO : tele_arg [tele] | TargS : forall (X : Type) (binder : X -> tele) (x : X), binder x -> TeleS binder
                                                                                                  ^ ????????   *)

Janno (Jun 12 2020 at 23:23):

Maybe I am just too tired to see that this is the way it's supposed to be.

Janno (Jun 12 2020 at 23:24):

Oh god, tele_arg is a coercion that is also being used when printing the coercion (i.e. itself).

Last updated: Dec 07 2023 at 14:02 UTC