aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coqdoc/links.v
blob: 581029bdd2b3fe1b6e16f7ef67d764933bafb6d9 (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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
(** Various checks for coqdoc

- symbols should not be inlined in string g
- links to both kinds of notations in a' should work to the right notation
- with utf8 option, forall must be unicode
- splitting between symbols and ident should be correct in a' and c
- ".." should be rendered correctly
*)

Require Import String.

Definition g := "dfjkh""sdfhj forall <> * ~"%string.

Definition a (b: nat) := b.

Definition f := forall C:Prop, C.

Notation "n ++ m" := (plus n m).

Notation "n ++ m" := (mult n m). (* redefinition *)

Notation "n ** m" := (plus n m) (at level 60).

Notation "n ▵ m" := (plus n m) (at level 60).

Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).

Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : x = x :>A

where "x = y :> A" := (@eq A x y) : type_scope.

Definition eq0 := 0 = 0 :> nat.

Notation "( x # y ; .. ; z )" := (pair .. (pair x y) .. z).

Definition b_α := ((0#0;0) , (0 ** 0)).

Notation h := a.

  Section test.

    Variables b' b2: nat.

    Notation "n + m" := (n ▵ m) : my_scope.

    Delimit Scope my_scope with my.

    Notation l := 0.

    Definition α := (0 + l)%my.

    Definition a' b := b'++0++b2 _ ++x b.

    Definition c := {True}+{True}.

    Definition d := (1+2)%nat.

    Lemma e : nat + nat.
    Admitted.

  End test.

  Section test2.

    Variables b': nat.

    Section test.

      Variables b2: nat.

      Definition a'' b := b' ++ O ++ b2 _ ++ x b + h 0.

    End test.

  End test2.

(** skip *)

(** skip *)

(** skip *)

(** skip *)

(** skip *)

(** skip *)

(** skip *)

(** skip *)

(** skip *)

(** skip *)

(** skip *)

(** skip *)

(** skip *)

(** skip *)