diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Decode/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Decode/index.html index 606d8fd4..928e6a13 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Decode/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Decode/index.html @@ -1,2 +1,2 @@ -Decode (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.Decode)

Module Bare.Decode

exception Error of string
type t = {
bs : bytes;
mutable off : int;
}
type 'a dec = t -> 'a
val fail_ : string -> 'a
val fail_eof_ : string -> 'a
val uint : t -> int64
val int : t -> int64
val u8 : t -> char
val i8 : t -> char
val u16 : t -> int
val i16 : t -> int
val u32 : t -> int32
val i32 : t -> int32
val u64 : t -> int64
val i64 : t -> int64
val bool : t -> bool
val f32 : t -> float
val f64 : t -> float
val data_of : size:int -> t -> bytes
val data : t -> bytes
val string : t -> string
val optional : (t -> 'a) -> t -> 'a option
\ No newline at end of file +Decode (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.Decode)

Module Bare.Decode

type t = input
val of_input : input -> t
val of_bytes : ?off:int -> ?len:int -> bytes -> t
val of_string : ?off:int -> ?len:int -> string -> t
type 'a dec = t -> 'a
val uint : t -> int64
val int : t -> int64
val i8 : t -> char
val u8 : t -> char
val i16 : t -> int
val u16 : t -> int
val i32 : t -> int32
val u32 : t -> int32
val i64 : t -> int64
val u64 : t -> int64
val bool : t -> bool
val f32 : t -> float
val f64 : t -> float
val data_of : size:int -> t -> bytes
val data : t -> bytes
val string : t -> string
val optional : (t -> 'a) -> t -> 'a option
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Encode/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Encode/index.html index a30f4c2f..aea5bde7 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Encode/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Encode/index.html @@ -1,2 +1,2 @@ -Encode (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.Encode)

Module Bare.Encode

type t = Stdlib.Buffer.t
val of_buffer : t -> t
type 'a enc = t -> 'a -> unit
val unsafe_chr : int -> char
val uint : t -> int64 -> unit
val int : t -> int64 -> unit
val u8 : Stdlib.Buffer.t -> char -> unit
val i8 : Stdlib.Buffer.t -> char -> unit
val u16 : Stdlib.Buffer.t -> int -> unit
val i16 : Stdlib.Buffer.t -> int -> unit
val u32 : Stdlib.Buffer.t -> int32 -> unit
val i32 : Stdlib.Buffer.t -> int32 -> unit
val u64 : Stdlib.Buffer.t -> int64 -> unit
val i64 : Stdlib.Buffer.t -> int64 -> unit
val bool : Stdlib.Buffer.t -> bool -> unit
val f64 : t -> float -> unit
val data_of : size:int -> Stdlib.Buffer.t -> bytes -> unit
val data : t -> bytes -> unit
val string : t -> string -> unit
val optional : (Stdlib.Buffer.t -> 'a -> unit) -> Stdlib.Buffer.t -> 'a option -> unit
\ No newline at end of file +Encode (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.Encode)

Module Bare.Encode

type t = output
val of_output : output -> t
val of_buffer : Stdlib.Buffer.t -> t
type 'a enc = t -> 'a -> unit
val unsafe_chr : int -> char
val uint : t -> int64 -> unit
val int : t -> int64 -> unit
val i8 : t -> char -> unit
val u8 : t -> char -> unit
val i16 : t -> int -> unit
val u16 : t -> int -> unit
val i32 : t -> int32 -> unit
val u32 : t -> int32 -> unit
val i64 : t -> int64 -> unit
val u64 : t -> int64 -> unit
val bool : t -> bool -> unit
val f64 : t -> float -> unit
val data_of : size:int -> t -> bytes -> unit
val data : t -> bytes -> unit
val string : t -> string -> unit
val optional : (t -> 'a -> unit) -> t -> 'a option -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/index.html index 43bc91b7..628709c6 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/index.html @@ -1,2 +1,2 @@ -Bare (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare)

Module Proof_ser.Bare

module String_map : sig ... end
val spf : ('a, unit, string) Stdlib.format -> 'a
module Decode : sig ... end
module Encode : sig ... end
module Pp : sig ... end
val to_string : 'a Encode.enc -> 'a -> string
val of_bytes_exn : ?off:int -> (Decode.t -> 'a) -> bytes -> 'a
val of_bytes : ?off:int -> (Decode.t -> 'a) -> bytes -> ('a, string) Stdlib.result
val of_string_exn : (Decode.t -> 'a) -> string -> 'a
val of_string : (Decode.t -> 'a) -> string -> ('a, string) Stdlib.result
\ No newline at end of file +Bare (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare)

Module Proof_ser.Bare

module String_map : sig ... end
module type INPUT = sig ... end
type input = (module INPUT)
val input_of_bytes : ?off:int -> ?len:int -> bytes -> input
module Decode : sig ... end
module type OUTPUT = sig ... end
type output = (module OUTPUT)
val output_of_buffer : Stdlib.Buffer.t -> output
module Encode : sig ... end
module Pp : sig ... end
val to_string : 'a Encode.enc -> 'a -> string
val of_bytes_exn : ?off:int -> ?len:int -> (Decode.t -> 'a) -> bytes -> 'a
val of_bytes : ?off:int -> ?len:int -> (Decode.t -> 'a) -> bytes -> ('a, string) Stdlib.result
val of_string_exn : ?off:int -> ?len:int -> (Decode.t -> 'a) -> string -> 'a
val of_string : ?off:int -> ?len:int -> (Decode.t -> 'a) -> string -> ('a, string) Stdlib.result
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-INPUT/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-INPUT/index.html new file mode 100644 index 00000000..5d4334aa --- /dev/null +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-INPUT/index.html @@ -0,0 +1,2 @@ + +INPUT (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.INPUT)

Module type Bare.INPUT

val read_byte : unit -> char
val read_i16 : unit -> int
val read_i32 : unit -> int32
val read_i64 : unit -> int64
val read_exact : bytes -> int -> int -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-OUTPUT/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-OUTPUT/index.html new file mode 100644 index 00000000..2e576c9c --- /dev/null +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-OUTPUT/index.html @@ -0,0 +1,2 @@ + +OUTPUT (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.OUTPUT)

Module type Bare.OUTPUT

val write_byte : char -> unit
val write_i16 : int -> unit
val write_i32 : int32 -> unit
val write_i64 : int64 -> unit
val write_exact : bytes -> int -> int -> unit
val flush : unit -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Clause/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Clause/index.html index 9093c632..b8805c3d 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Clause/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Clause/index.html @@ -1,2 +1,2 @@ -Clause (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Clause)

Module Proof_ser.Clause

type t = {
lits : Lit.t array;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Clause (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Clause)

Module Proof_ser.Clause

type t = {
lits : Lit.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_app/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_app/index.html index 40c41dd8..13d0d9df 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_app/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_app/index.html @@ -1,2 +1,2 @@ -Expr_app (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_app)

Module Proof_ser.Expr_app

type t = {
f : ID.t;
args : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Expr_app (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_app)

Module Proof_ser.Expr_app

type t = {
f : ID.t;
args : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_bool/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_bool/index.html index 6f66b789..d636dc89 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_bool/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_bool/index.html @@ -1,2 +1,2 @@ -Expr_bool (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_bool)

Module Proof_ser.Expr_bool

type t = {
b : bool;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Expr_bool (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_bool)

Module Proof_ser.Expr_bool

type t = {
b : bool;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_def/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_def/index.html index 70083b0b..ad326eec 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_def/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_def/index.html @@ -1,2 +1,2 @@ -Expr_def (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_def)

Module Proof_ser.Expr_def

type t = {
c : ID.t;
rhs : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Expr_def (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_def)

Module Proof_ser.Expr_def

type t = {
c : ID.t;
rhs : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_eq/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_eq/index.html index e89da8a2..1b13c578 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_eq/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_eq/index.html @@ -1,2 +1,2 @@ -Expr_eq (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_eq)

Module Proof_ser.Expr_eq

type t = {
lhs : ID.t;
rhs : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Expr_eq (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_eq)

Module Proof_ser.Expr_eq

type t = {
lhs : ID.t;
rhs : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_if/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_if/index.html index 8000a6bd..5cf5a509 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_if/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_if/index.html @@ -1,2 +1,2 @@ -Expr_if (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_if)

Module Proof_ser.Expr_if

type t = {
cond : ID.t;
then_ : ID.t;
else_ : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Expr_if (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_if)

Module Proof_ser.Expr_if

type t = {
cond : ID.t;
then_ : ID.t;
else_ : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_isa/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_isa/index.html index c14d4666..fbba7470 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_isa/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_isa/index.html @@ -1,2 +1,2 @@ -Expr_isa (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_isa)

Module Proof_ser.Expr_isa

type t = {
c : ID.t;
arg : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Expr_isa (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_isa)

Module Proof_ser.Expr_isa

type t = {
c : ID.t;
arg : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_not/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_not/index.html index fa1e8b42..1ca24529 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_not/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_not/index.html @@ -1,2 +1,2 @@ -Expr_not (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_not)

Module Proof_ser.Expr_not

type t = {
f : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Expr_not (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_not)

Module Proof_ser.Expr_not

type t = {
f : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Fun_decl/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Fun_decl/index.html index 1d44d1df..f0ab2037 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Fun_decl/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Fun_decl/index.html @@ -1,2 +1,2 @@ -Fun_decl (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Fun_decl)

Module Proof_ser.Fun_decl

type t = {
f : string;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Fun_decl (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Fun_decl)

Module Proof_ser.Fun_decl

type t = {
f : string;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/ID/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/ID/index.html index 4f95203f..3af17fc0 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/ID/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/ID/index.html @@ -1,2 +1,2 @@ -ID (sidekick-base.Sidekick_base_proof_trace.Proof_ser.ID)

Module Proof_ser.ID

type t = int32
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +ID (sidekick-base.Sidekick_base_proof_trace.Proof_ser.ID)

Module Proof_ser.ID

type t = int32
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Lit/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Lit/index.html index b000c326..70d2c4b7 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Lit)

Module Proof_ser.Lit

type t = ID.t
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Lit)

Module Proof_ser.Lit

type t = ID.t
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step/index.html index 94da1acf..6eb2a45f 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step/index.html @@ -1,2 +1,2 @@ -Step (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step)

Module Proof_ser.Step

type t = {
id : ID.t;
view : Step_view.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step)

Module Proof_ser.Step

type t = {
id : ID.t;
view : Step_view.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_c/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_c/index.html index 23e6a756..edb19ea6 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_c/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_c/index.html @@ -1,2 +1,2 @@ -Step_bool_c (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_bool_c)

Module Proof_ser.Step_bool_c

type t = {
rule : string;
exprs : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_bool_c (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_bool_c)

Module Proof_ser.Step_bool_c

type t = {
rule : string;
exprs : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_tauto/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_tauto/index.html index 086b3aaa..b13785c4 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_tauto/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_tauto/index.html @@ -1,2 +1,2 @@ -Step_bool_tauto (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_bool_tauto)

Module Proof_ser.Step_bool_tauto

type t = {
lits : Lit.t array;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_bool_tauto (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_bool_tauto)

Module Proof_ser.Step_bool_tauto

type t = {
lits : Lit.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bridge_lit_expr/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bridge_lit_expr/index.html index 7c444c2e..a7e1e3c4 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bridge_lit_expr/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bridge_lit_expr/index.html @@ -1,2 +1,2 @@ -Step_bridge_lit_expr (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_bridge_lit_expr)

Module Proof_ser.Step_bridge_lit_expr

type t = {
lit : Lit.t;
expr : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_bridge_lit_expr (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_bridge_lit_expr)

Module Proof_ser.Step_bridge_lit_expr

type t = {
lit : Lit.t;
expr : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_cc/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_cc/index.html index 432ba14d..ca30badc 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_cc/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_cc/index.html @@ -1,2 +1,2 @@ -Step_cc (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_cc)

Module Proof_ser.Step_cc

type t = {
eqns : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_cc (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_cc)

Module Proof_ser.Step_cc

type t = {
eqns : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_clause_rw/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_clause_rw/index.html index 695a44c5..062eb06c 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_clause_rw/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_clause_rw/index.html @@ -1,2 +1,2 @@ -Step_clause_rw (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_clause_rw)

Module Proof_ser.Step_clause_rw

type t = {
c : ID.t;
res : Clause.t;
using : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_clause_rw (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_clause_rw)

Module Proof_ser.Step_clause_rw

type t = {
c : ID.t;
res : Clause.t;
using : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_input/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_input/index.html index b658093b..dd80b7d1 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_input/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_input/index.html @@ -1,2 +1,2 @@ -Step_input (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_input)

Module Proof_ser.Step_input

type t = {
c : Clause.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_input (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_input)

Module Proof_ser.Step_input

type t = {
c : Clause.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_preprocess/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_preprocess/index.html index e4212b9c..d1c916b9 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_preprocess/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_preprocess/index.html @@ -1,2 +1,2 @@ -Step_preprocess (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_preprocess)

Module Proof_ser.Step_preprocess

type t = {
t : ID.t;
u : ID.t;
using : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_preprocess (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_preprocess)

Module Proof_ser.Step_preprocess

type t = {
t : ID.t;
u : ID.t;
using : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_p1/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_p1/index.html index b3fa1d63..472e5649 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_p1/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_p1/index.html @@ -1,2 +1,2 @@ -Step_proof_p1 (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_proof_p1)

Module Proof_ser.Step_proof_p1

type t = {
rw_with : ID.t;
c : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_proof_p1 (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_proof_p1)

Module Proof_ser.Step_proof_p1

type t = {
rw_with : ID.t;
c : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_r1/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_r1/index.html index ea5323cd..39bf399a 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_r1/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_r1/index.html @@ -1,2 +1,2 @@ -Step_proof_r1 (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_proof_r1)

Module Proof_ser.Step_proof_r1

type t = {
unit : ID.t;
c : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_proof_r1 (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_proof_r1)

Module Proof_ser.Step_proof_r1

type t = {
unit : ID.t;
c : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_res/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_res/index.html index febbe36f..14bf428b 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_res/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_res/index.html @@ -1,2 +1,2 @@ -Step_proof_res (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_proof_res)

Module Proof_ser.Step_proof_res

type t = {
pivot : ID.t;
c1 : ID.t;
c2 : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_proof_res (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_proof_res)

Module Proof_ser.Step_proof_res

type t = {
pivot : ID.t;
c1 : ID.t;
c2 : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_rup/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_rup/index.html index 4bdb78e3..4e782189 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_rup/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_rup/index.html @@ -1,2 +1,2 @@ -Step_rup (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_rup)

Module Proof_ser.Step_rup

type t = {
res : Clause.t;
hyps : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_rup (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_rup)

Module Proof_ser.Step_rup

type t = {
res : Clause.t;
hyps : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_true/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_true/index.html index e44019fe..5095ff5e 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_true/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_true/index.html @@ -1,2 +1,2 @@ -Step_true (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_true)

Module Proof_ser.Step_true

type t = {
true_ : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_true (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_true)

Module Proof_ser.Step_true

type t = {
true_ : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_unsat/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_unsat/index.html index c725ba62..d7a2a0c0 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_unsat/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_unsat/index.html @@ -1,2 +1,2 @@ -Step_unsat (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_unsat)

Module Proof_ser.Step_unsat

type t = {
c : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_unsat (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_unsat)

Module Proof_ser.Step_unsat

type t = {
c : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_view/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_view/index.html index 032422a0..73525069 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_view/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_view/index.html @@ -1,2 +1,2 @@ -Step_view (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_view)

Module Proof_ser.Step_view

type t =
| Step_input of Step_input.t
| Step_unsat of Step_unsat.t
| Step_rup of Step_rup.t
| Step_bridge_lit_expr of Step_bridge_lit_expr.t
| Step_cc of Step_cc.t
| Step_preprocess of Step_preprocess.t
| Step_clause_rw of Step_clause_rw.t
| Step_bool_tauto of Step_bool_tauto.t
| Step_bool_c of Step_bool_c.t
| Step_proof_p1 of Step_proof_p1.t
| Step_proof_r1 of Step_proof_r1.t
| Step_proof_res of Step_proof_res.t
| Step_true of Step_true.t
| Fun_decl of Fun_decl.t
| Expr_def of Expr_def.t
| Expr_bool of Expr_bool.t
| Expr_if of Expr_if.t
| Expr_not of Expr_not.t
| Expr_isa of Expr_isa.t
| Expr_eq of Expr_eq.t
| Expr_app of Expr_app.t
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_view (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_view)

Module Proof_ser.Step_view

type t =
| Step_input of Step_input.t
| Step_unsat of Step_unsat.t
| Step_rup of Step_rup.t
| Step_bridge_lit_expr of Step_bridge_lit_expr.t
| Step_cc of Step_cc.t
| Step_preprocess of Step_preprocess.t
| Step_clause_rw of Step_clause_rw.t
| Step_bool_tauto of Step_bool_tauto.t
| Step_bool_c of Step_bool_c.t
| Step_proof_p1 of Step_proof_p1.t
| Step_proof_r1 of Step_proof_r1.t
| Step_proof_res of Step_proof_res.t
| Step_true of Step_true.t
| Fun_decl of Fun_decl.t
| Expr_def of Expr_def.t
| Expr_bool of Expr_bool.t
| Expr_if of Expr_if.t
| Expr_not of Expr_not.t
| Expr_isa of Expr_isa.t
| Expr_eq of Expr_eq.t
| Expr_app of Expr_app.t
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file