|
Set Implicit Arguments.
Ltac ret_and_left T :=
let t := type of T in
lazymatch eval hnf in t with
| ?a /\ ?b => constr:(proj1 T)
| forall x : ?T', @?f x =>
constr:(fun x : T' => ltac:(let fx := constr:(T x) in
let t := ret_and_left fx in
exact t))
end.
¤ Dauer der Verarbeitung: 0.0 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.
|
