Показать оригинальное имя импортированного модуля в Coq

Question

Как выбрать текстовое представление переменных, которое принадлежит какому-либо модулю?(Пожалуйста, смотрите комментарии внутри кода ниже. Это похоже на нотацию для модулей.) Я хочу использовать это, потому что желательно видеть первоначальное значение терминов.(и отдельные типы с одинаковой реализацией: SetVars.t, FuncSymb.t, PredSymb.t и т. д.)

Require Import Coq.Structures.Equalities.
Require Import Arith.PeanoNat.
Module mod1 (SetVars : UsualDecidableTypeFull).
Definition h:SetVars.t->SetVars.t := fun x => x. (*example*)
End mod1.

Module mod2.
Module SetVars := PeanoNat.Nat.
Module X := mod1 SetVars.
Import X.
Theorem q:SetVars.t->SetVars.t.
Proof. exact h. Defined. (* Here everything is OK *)
Check h. (*"h : nat -> nat"*)
(*But I want to see "h:SetVars.t->SetVars.t"*)
End mod2.

Answer 1

Заменить

Module SetVars := PeanoNat.Nat.

на

Module SetVars : UsualDecidableTypeFull := PeanoNat.Nat.

Это делает модуль SetVars непрозрачным, выставляя точно сигнатуру UsualDecidableTypeFull, так что тип SetVars.t -> SetVars.t больше не можетбыть уменьшенным.