1type "HOL4.min.ind" as "ind"
2const "HOL4.min.@" as "select"
3const "HOL4.bool.!" as "Data.Bool.!"
4const "HOL4.bool.?" as "Data.Bool.?"
5const "HOL4.bool.?!" as "Data.Bool.?!"
6const "HOL4.bool.T" as "Data.Bool.T"
7const "HOL4.bool.F" as "Data.Bool.F"
8const "HOL4.bool./\\" as "Data.Bool./\\"
9const "HOL4.bool.\\/" as "Data.Bool.\\/"
10const "HOL4.min.==>" as "Data.Bool.==>"
11const "HOL4.bool.~" as "Data.Bool.~"
12const "HOL4.bool.COND" as "Data.Bool.cond"
13const "HOL4.bool.ONE_ONE" as "Function.injective"
14const "HOL4.bool.ONTO" as "Function.surjective"
15
16const "HOL4.combin.o" as "Function.o"
17const "HOL4.combin.K" as "Function.const"
18const "HOL4.combin.I" as "Function.id"
19const "HOL4.combin.C" as "Function.flip"
20const "HOL4.combin.S" as "Function.Combinator.s"
21const "HOL4.combin.W" as "Function.Combinator.w"
22
23const "HOL4.relation.TC" as "Relation.transitiveClosure"
24const "HOL4.relation.reflexive" as "Relation.reflexive"
25const "HOL4.relation.irreflexive" as "Relation.irreflexive"
26const "HOL4.relation.transitive" as "Relation.transitive"
27const "HOL4.relation.RUNION" as "Relation.union"
28const "HOL4.relation.RINTER" as "Relation.intersect"
29const "HOL4.relation.RUNIV" as "Relation.universe"
30const "HOL4.relation.EMPTY_REL" as "Relation.empty"
31const "HOL4.relation.RSUBSET" as "Relation.subrelation"
32const "HOL4.relation.WF" as "Relation.wellFounded"
33
34type "HOL4.option.option" as "Data.Option.option"
35const "HOL4.option.SOME" as "Data.Option.some"
36const "HOL4.option.NONE" as "Data.Option.none"
37const "HOL4.option.IS_NONE" as "Data.Option.isNone"
38const "HOL4.option.IS_SOME" as "Data.Option.isSome"
39const "HOL4.option.OPTION_MAP" as "Data.Option.map"
40
41type "HOL4.one.one" as "Data.Unit.unit"
42const "HOL4.one.one" as "Data.Unit.()"
43
44type "HOL4.sum.sum" as "Data.Sum.+"
45const "HOL4.sum.INL" as "Data.Sum.left"
46const "HOL4.sum.INR" as "Data.Sum.right"
47const "HOL4.sum.ISL" as "Data.Sum.isLeft"
48const "HOL4.sum.ISR" as "Data.Sum.isRight"
49const "HOL4.sum.OUTL" as "Data.Sum.destLeft"
50const "HOL4.sum.OUTR" as "Data.Sum.destRight"
51
52type "HOL4.pair.prod" as "Data.Pair.*"
53const "HOL4.pair.," as "Data.Pair.,"
54const "HOL4.pair.FST" as "Data.Pair.fst"
55const "HOL4.pair.SND" as "Data.Pair.snd"
56
57type "HOL4.num.num" as "Number.Natural.natural"
58const "HOL4.num.0" as "Number.Natural.zero"
59const "HOL4.num.SUC" as "Number.Natural.suc"
60const "HOL4.prim_rec.<" as "Number.Natural.<"
61
62const "HOL4.arithmetic.*" as "Number.Natural.*"
63const "HOL4.arithmetic.+" as "Number.Natural.+"
64const "HOL4.arithmetic.<=" as "Number.Natural.<="
65const "HOL4.arithmetic.>" as "Number.Natural.>"
66const "HOL4.arithmetic.>=" as "Number.Natural.>="
67const "HOL4.arithmetic.MIN" as "Number.Natural.min"
68const "HOL4.arithmetic.MAX" as "Number.Natural.max"
69const "HOL4.arithmetic.DIV" as "Number.Natural.div"
70const "HOL4.arithmetic.MOD" as "Number.Natural.mod"
71const "HOL4.arithmetic.EVEN" as "Number.Natural.even"
72const "HOL4.arithmetic.ODD" as "Number.Natural.odd"
73const "HOL4.arithmetic.LOG" as "Number.Natural.log"
74const "HOL4.arithmetic.EXP" as "Number.Natural.^"
75const "HOL4.arithmetic.FACT" as "Number.Natural.factorial"
76const "HOL4.arithmetic.BIT1" as "Number.Natural.bit1"
77const "HOL4.arithmetic.ZERO" as "Number.Natural.zero"
78const "HOL4.numeralConv.BIT0" as "Number.Natural.bit0"
79
80type "HOL4.list.list" as "Data.List.list"
81const "HOL4.list.NIL" as "Data.List.[]"
82const "HOL4.list.CONS" as "Data.List.::"
83const "HOL4.list.LENGTH" as "Data.List.length"
84const "HOL4.list.APPEND" as "Data.List.@"
85const "HOL4.list.MAP" as "Data.List.map"
86const "HOL4.list.REVERSE" as "Data.List.reverse"
87const "HOL4.list.HD" as "Data.List.head"
88const "HOL4.list.TL" as "Data.List.tail"
89const "HOL4.list.EVERY" as "Data.List.all"
90const "HOL4.list.EXISTS" as "Data.List.any"
91const "HOL4.list.FLAT" as "Data.List.concat"
92const "HOL4.list.FILTER" as "Data.List.filter"
93const "HOL4.list.NULL" as "Data.List.null"
94const "HOL4.list.LAST" as "Data.List.last"
95const "HOL4.list.UNZIP" as "Data.List.unzip"
96
97type "HOL4.realax.real" as "Number.Real.real"
98const "HOL4.realax.real_add" as "Number.Real.+"
99const "HOL4.realax.real_lt" as "Number.Real.<"
100const "HOL4.realax.real_mul" as "Number.Real.*"
101const "HOL4.realax.real_neg" as "Number.Real.~"
102const "HOL4.real.abs" as "Number.Real.abs"
103const "HOL4.real.max" as "Number.Real.max"
104const "HOL4.real.min" as "Number.Real.min"
105const "HOL4.real.pow" as "Number.Real.^"
106const "HOL4.real.real_ge" as "Number.Real.>="
107const "HOL4.real.real_gt" as "Number.Real.>"
108const "HOL4.real.real_lte" as "Number.Real.<="
109const "HOL4.real.real_of_num" as "Number.Real.fromNatural"
110const "HOL4.real.real_sub" as "Number.Real.-"
111