blob: 7d0dc090e1559e5df26f132e83189e1a11d55522 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* -*- coq-prog-args: ("-emacs" "-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 arugments to [compose] *)
|
