blob: 86420bd8c8b89415dc598802cd08e77157638eb4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
Set Implicit Arguments.
Unset Strict Implicit.
(* Suggested by Pierre Casteran (BZ#169) *)
(* Argument 3 is needed to typecheck and should be printed *)
Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x).
Check (compose (C:=nat) S).
(* Better to explicitly display the arguments inferable from a
position that could disappear after reduction *)
Inductive ex (A : Set) (P : A -> Prop) : Prop :=
ex_intro : forall x : A, P x -> ex P.
Check (ex_intro (P:=fun _ => True) (x:=0) I).
(* Test for V8 printing of implicit by names *)
Definition d1 y x (h : x = y :>nat) := h.
Definition d2 x := d1 (y:=x).
Print d2.
Set Strict Implicit.
Unset Implicit Arguments.
(* Check maximal insertion of implicit *)
Require Import List.
Open Scope list_scope.
Set Implicit Arguments.
Set Maximal Implicit Insertion.
Definition id (A:Type) (x:A) := x.
Check map id (1::nil).
Definition id' (A:Type) (x:A) := x.
Arguments id' {A} x.
Check map id' (1::nil).
Unset Maximal Implicit Insertion.
Unset Implicit Arguments.
(* Check explicit insertion of last non-maximal trailing implicit to ensure *)
(* correct arity of partiol applications *)
Set Implicit Arguments.
Definition id'' (A:Type) (x:A) := x.
Check map (@id'' nat) (1::nil).
Module MatchBranchesInContext.
Set Implicit Arguments.
Set Contextual Implicit.
Inductive option A := None | Some (a:A).
Coercion some_nat := @Some nat.
Check fix f x := match x with 0 => None | n => some_nat n end.
End MatchBranchesInContext.
Module LetInContext.
Set Implicit Arguments.
Set Contextual Implicit.
Axiom False_rect : forall A:Type, False -> A.
Check fun x:False => let y:= False_rect (A:=bool) x in y. (* will not be in context: explicitation *)
Check fun x:False => let y:= False_rect (A:=True) x in y. (* will be in context: no explicitation *)
End LetInContext.
|
