-
Notifications
You must be signed in to change notification settings - Fork 9
/
Copy pathAxiomatizedTypes.v
125 lines (91 loc) · 2.53 KB
/
AxiomatizedTypes.v
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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
Require GHC.Base.
Require HsToCoq.Err.
Axiom Coercion : Type.
Axiom Type_ : Type.
Axiom ThetaType : Type.
Axiom TyBinder : Type.
Axiom TyThing : Type.
Definition Kind : Type := Type_.
Definition PredType : Type := Type_.
Axiom BranchFlag : Type.
Axiom CoAxiom : BranchFlag -> Type.
Axiom Branched : BranchFlag.
Axiom Unbranched : BranchFlag.
Axiom BuiltInSynFamily : Type.
Axiom BranchIndex : Type.
Axiom CoAxiomRule : Type.
Axiom CoAxBranch : Type.
Inductive Role : Type := Representational | Nominal | Phantom.
Axiom TcTyVarDetails : Type.
Axiom liftedTypeKind : Kind.
Axiom constraintKind : Kind.
Axiom PrimOp : Type.
Axiom ForeignCall : Type.
Axiom CType : Type.
Axiom CostCentre : Type.
Axiom DataConBoxer : Type.
(* -------------------- assumed default instances ------------------- *)
Instance Default__Coercion
: HsToCoq.Err.Default Coercion.
Admitted.
Instance Default__Type_
: HsToCoq.Err.Default Type_.
Admitted.
Instance Default__ThetaType
: HsToCoq.Err.Default ThetaType.
Admitted.
Instance Default__TyBinder
: HsToCoq.Err.Default TyBinder.
Admitted.
Instance Default__TyThing
: HsToCoq.Err.Default TyThing.
Admitted.
Instance Default__CoAxiom
: forall {a}, HsToCoq.Err.Default (CoAxiom a).
Admitted.
Instance Default__BuiltInSynFamily
: HsToCoq.Err.Default BuiltInSynFamily.
Admitted.
Instance Default__TcTyVarDetails
: HsToCoq.Err.Default TcTyVarDetails.
Admitted.
Instance Default__Role
: HsToCoq.Err.Default Role.
Admitted.
Instance Default__BranchIndex
: HsToCoq.Err.Default BranchIndex.
Admitted.
Instance Default__CoAxiomRule
: HsToCoq.Err.Default CoAxiomRule.
Admitted.
Instance Default__CoAxiomBranch
: HsToCoq.Err.Default CoAxBranch.
Admitted.
Instance Default__CostCentre
: HsToCoq.Err.Default CostCentre.
Admitted.
Instance Default__DataConBoxer
: HsToCoq.Err.Default DataConBoxer.
Admitted.
Instance Default__PrimOp
: HsToCoq.Err.Default PrimOp.
Admitted.
Instance Default__ForeignCall
: HsToCoq.Err.Default ForeignCall.
Admitted.
Instance Default__CType
: HsToCoq.Err.Default CType.
Admitted.
(* ---------------- Eq -------------- *)
Instance Eq___CoAxiomRule
: GHC.Base.Eq_ CoAxiomRule.
Admitted.
Instance Eq___Role
: GHC.Base.Eq_ Role.
Admitted.
Instance Eq___CostCentre
: GHC.Base.Eq_ CostCentre.
Admitted.
Instance Ord___CostCentre
: GHC.Base.Ord CostCentre.
Admitted.