nested-eliminators/_RocqProject at main · MetaRocq/nested-eliminators · GitHub

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
-arg "-w '-notation-overridden'" -Q ./theories MetaRocq.NestedElim -Q ./formalization MetaRocq.NestedElim.Formalization
# -arg "-output-directory ."

# Formalization
formalization/Lemma.v
formalization/Positivity_condition.v
formalization/Nested_to_mutual.v
formalization/Nested_to_mutual_proof.v
formalization/RoseTree.v
formalization/typing.v

# API
theories/API/core.v
theories/API/fold_functions.v
theories/API/debug_functions.v
# API: inductive
theories/API/inductive_access.v
theories/API/inductive_store.v
# API: context
theories/API/context_access.v
theories/API/context_store.v
# API: create terms
theories/API/creating_terms.v
theories/API/read_mode_ind.v
theories/API/decide.v
# API: views
theories/API/view_args.v
# API: All
theories/API/api_debruijn.v

# Preproccess data
theories/Preprocess/uniform_parameters.v
theories/Preprocess/strictly_positive_uniform_parameters.v

# Eliminators
theories/Eliminators/eliminators.v

# Custom Parametricity
theories/SparseParametricity/sparse_parametricity_rec_hyp.v
theories/SparseParametricity/sparse_parametricity.v
theories/SparseParametricity/local_fundamental_lemma.v

# Tests
theories/test_functions.v
theories/examples.v