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
^ ???????? *)
Maybe I am just too tired to see that this is the way it's supposed to be.
Oh god, tele_arg
is a coercion that is also being used when printing the coercion (i.e. itself).
Last updated: Jun 09 2023 at 07:01 UTC