Unnamed repository; edit this file 'description' to name the repository.
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
|
; TLA⁺ scopes and definitions
[
(bounded_quantification)
(choose)
(function_definition)
(function_literal)
(lambda)
(let_in)
(module)
(module_definition)
(operator_definition)
(set_filter)
(set_map)
(unbounded_quantification)
] @local.scope
; Definitions
(choose (identifier) @local.definition.variable.parameter)
(choose (tuple_of_identifiers (identifier) @local.definition.variable.parameter))
(constant_declaration (identifier) @local.definition.constant)
(constant_declaration (operator_declaration name: (_) @local.definition.constant))
(function_definition name: (identifier) @local.definition.function)
(lambda (identifier) @local.definition.function)
(module_definition name: (_) @local.definition.namespace)
(module_definition parameter: (identifier) @local.definition.variable.parameter)
(module_definition parameter: (operator_declaration name: (_) @local.definition.variable.parameter))
(operator_definition name: (_) @local.definition.operator)
(operator_definition parameter: (identifier) @local.definition.variable.parameter)
(operator_definition parameter: (operator_declaration name: (_) @local.definition.variable.parameter))
(quantifier_bound (identifier) @local.definition.variable.parameter)
(quantifier_bound (tuple_of_identifiers (identifier) @local.definition.variable.parameter))
(unbounded_quantification (identifier) @local.definition.variable.parameter)
(variable_declaration (identifier) @local.definition.variable.builtin)
; Proof scopes and definitions
[
(non_terminal_proof)
(suffices_proof_step)
(theorem)
] @local.scope
(assume_prove (new (identifier) @local.definition.variable.parameter))
(assume_prove (new (operator_declaration name: (_) @local.definition.variable.parameter)))
(assumption name: (identifier) @local.definition.constant)
(pick_proof_step (identifier) @local.definition.variable.parameter)
(take_proof_step (identifier) @local.definition.variable.parameter)
(theorem name: (identifier) @local.definition.constant)
;PlusCal scopes and definitions
[
(pcal_algorithm)
(pcal_macro)
(pcal_procedure)
(pcal_with)
] @local.scope
(pcal_macro_decl parameter: (identifier) @local.definition.variable.parameter)
(pcal_proc_var_decl (identifier) @local.definition.variable.parameter)
(pcal_var_decl (identifier) @local.definition.variable.parameter)
(pcal_with (identifier) @local.definition.variable.parameter)
; References
(identifier_ref) @local.reference
((prefix_op_symbol) @local.reference)
(bound_prefix_op symbol: (_) @local.reference)
((infix_op_symbol) @local.reference)
(bound_infix_op symbol: (_) @local.reference)
((postfix_op_symbol) @local.reference)
(bound_postfix_op symbol: (_) @local.reference)
(bound_nonfix_op symbol: (_) @local.reference)
|