blob: 129a5117c96d389312465fc546bf41b6d3784197 (
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
|
(**
<<
uint32_t shift_right( uint32_t a, uint32_t shift )
{
return a >> shift;
}
>>
This line and the following shows << verbatim >> text:
<< A stand-alone inline verbatim >>
<< A non-ended inline verbatim to test line location
- item 1
- item 2 is <<verbatim>>
- item 3 is <<verbatim>> too
[[
A coq block : forall n, n = 0
]]
- <<verbatim>> again, and a formula [ True -> False ]
-
<<
multiline
verbatim
>>
- last item
[[[
Γ ⊢ A
----
Γ ⊢ A ∨ B
]]]
<<
A non-ended block verbatim to test line location
*)
|
