|
Record foo : Type :=
{ fooA : Type; fooB : Type }.
Definition id {A : Type} (a : A) := a.
Definition untypable : Type.
unshelve refine (let X := _ in let Y : _ := ltac:(let ty := type of X in exact ty) in id Y).
exact foo.
constructor. exact unit. exact unit.
Defined.
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
