|
(* -*- coq-prog-args: ("-nois") -*- *)
Delimit Scope type_scope with type.
Delimit Scope function_scope with function.
Bind Scope type_scope with Sortclass.
Bind Scope function_scope with Funclass.
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Definition compose {A B C} (g : B -> C) (f : A -> B) :=
fun x : A => g (f x).
Notation " g ∘ f " := (compose g f)
(at level 40, left associativity) : function_scope.
Fail Check (fun x => x) ∘ (fun x => x). (* this [Check] should fail, as [function_scope] is not opened *)
Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arguments to [compose] *)
¤ 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.
|
