Structure HOLsexp
signature HOLsexp =
sig
datatype t = datatype HOLsexp_dtype.t
type 'a encoder = 'a -> t
type 'a decoder = t -> 'a option
val Nil : t
val Quote : t
val List : t list -> t
val strip_list : t -> t list * t option
val dest_tagged : string -> t -> t option
val tagged_encode : string -> 'a encoder -> 'a encoder
val list_encode : 'a encoder -> 'a list encoder
val pair_encode : ('a encoder * 'b encoder) -> ('a * 'b) encoder
val pair3_encode : ('a encoder * 'b encoder * 'c encoder) ->
('a * 'b * 'c) encoder
val pair4_encode : ('a encoder * 'b encoder * 'c encoder * 'd encoder) ->
('a * 'b * 'c * 'd) encoder
val int_decode : int decoder
val symbol_decode : string decoder
val string_decode : string decoder
val pair_decode : 'a decoder * 'b decoder -> ('a * 'b) decoder
val pair3_decode : 'a decoder * 'b decoder * 'c decoder ->
('a * 'b * 'c) decoder
val pair4_decode : 'a decoder * 'b decoder * 'c decoder * 'd decoder ->
('a * 'b * 'c * 'd) decoder
val list_decode : 'a decoder -> 'a list decoder
val tagged_decode : string -> 'a decoder -> 'a decoder
val printer : t HOLPP.pprinter
val scan : (char, 'a) StringCvt.reader -> (t, 'a) StringCvt.reader
val fromString : string -> t option
val fromStream : TextIO.instream -> t
val fromFile : string -> t (* various possible failure to read exceptions *)
end
HOL 4, Trindemossen-1