-
Notifications
You must be signed in to change notification settings - Fork 3
/
_CoqProject
80 lines (69 loc) · 2.22 KB
/
_CoqProject
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
-R coq-partialfun/theories PartialFun
-Q theories LogRel
theories/Utils.v
theories/BasicAst.v
theories/AutoSubst/core.v
theories/AutoSubst/unscoped.v
theories/AutoSubst/Ast.v
theories/AutoSubst/Extra.v
theories/Context.v
theories/Notations.v
theories/NormalForms.v
theories/Weakening.v
theories/UntypedReduction.v
theories/UntypedValues.v
theories/GenericTyping.v
theories/DeclarativeTyping.v
theories/DeclarativeInstance.v
theories/LogicalRelation.v
theories/LogicalRelation/Induction.v
theories/LogicalRelation/Escape.v
theories/LogicalRelation/ShapeView.v
theories/LogicalRelation/Reflexivity.v
theories/LogicalRelation/Irrelevance.v
theories/LogicalRelation/Weakening.v
theories/LogicalRelation/Universe.v
theories/LogicalRelation/Neutral.v
theories/LogicalRelation/Transitivity.v
theories/LogicalRelation/Reduction.v
theories/LogicalRelation/NormalRed.v
theories/LogicalRelation/Application.v
theories/LogicalRelation/SimpleArr.v
theories/LogicalRelation/Id.v
theories/Validity.v
theories/Substitution/Irrelevance.v
theories/Substitution/Properties.v
theories/Substitution/Escape.v
theories/Substitution/Conversion.v
theories/Substitution/Reflexivity.v
theories/Substitution/Reduction.v
theories/Substitution/SingleSubst.v
theories/Substitution/Introductions/Application.v
theories/Substitution/Introductions/Universe.v
theories/Substitution/Introductions/Poly.v
theories/Substitution/Introductions/Pi.v
theories/Substitution/Introductions/Lambda.v
theories/Substitution/Introductions/SimpleArr.v
theories/Substitution/Introductions/Var.v
theories/Substitution/Introductions/Nat.v
theories/Substitution/Introductions/Empty.v
theories/Substitution/Introductions/Sigma.v
theories/Substitution/Introductions/Id.v
theories/Fundamental.v
theories/AlgorithmicTyping.v
theories/DeclarativeSubst.v
theories/TypeConstructorsInj.v
theories/Normalisation.v
theories/Consequences.v
theories/BundledAlgorithmicTyping.v
theories/AlgorithmicConvProperties.v
theories/AlgorithmicTypingProperties.v
theories/TypeUniqueness.v
theories/Decidability/Functions.v
theories/Decidability/Soundness.v
theories/Decidability/Completeness.v
theories/Decidability/Termination.v
theories/Decidability.v
theories/TermNotations.v
theories/Decidability/Execution.v
theories/Positivity.v