Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
inductive_functor_template.v
Sprache: Unknown
|
Module Type E. Parameter T : Type. End E.
Module F (X:E).
Inductive foo := box : X.T -> foo.
End F.
Module ME. Definition T := nat. End ME.
Module A := F ME.
(* Note: A.foo could live in Set, and coqchk sees that (because of
template polymorphism implementation details) *)
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
|
