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