From 45845072af8f2b482377c369fb44beb4353f5870 Mon Sep 17 00:00:00 2001 From: c-cube Date: Tue, 28 Dec 2021 21:48:24 +0000 Subject: [PATCH] deploy: be1c1573b15a68c22fee1d327a68ab719949a8c9 --- .../Sidekick_base_proof_trace/Proof_ser/Expr_isa/index.html | 2 ++ .../Sidekick_base_proof_trace/Proof_ser/Step_view/index.html | 2 +- .../Sidekick_base_proof_trace/Proof_ser/index.html | 2 +- dev/sidekick/Sidekick_quip/Proof/T/index.html | 2 +- 4 files changed, 5 insertions(+), 3 deletions(-) create mode 100644 dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_isa/index.html 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 new file mode 100644 index 00000000..c14d4666 --- /dev/null +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_isa/index.html @@ -0,0 +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 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 b77c7a88..b951baa8 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_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_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_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 diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/index.html index e585f896..12721353 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/index.html @@ -1,2 +1,2 @@ -Proof_ser (sidekick-base.Sidekick_base_proof_trace.Proof_ser)

Module Sidekick_base_proof_trace.Proof_ser

module Bare : sig ... end
module ID : sig ... end
module Lit : sig ... end
module Clause : sig ... end
module Step_input : sig ... end
module Step_rup : sig ... end
module Step_bridge_lit_expr : sig ... end
module Step_cc : sig ... end
module Step_preprocess : sig ... end
module Step_clause_rw : sig ... end
module Step_unsat : sig ... end
module Step_proof_p1 : sig ... end
module Step_proof_r1 : sig ... end
module Step_bool_tauto : sig ... end
module Step_bool_c : sig ... end
module Step_true : sig ... end
module Fun_decl : sig ... end
module Expr_def : sig ... end
module Expr_bool : sig ... end
module Expr_if : sig ... end
module Expr_not : sig ... end
module Expr_eq : sig ... end
module Expr_app : sig ... end
module Step_view : sig ... end
module Step : sig ... end
\ No newline at end of file +Proof_ser (sidekick-base.Sidekick_base_proof_trace.Proof_ser)

Module Sidekick_base_proof_trace.Proof_ser

module Bare : sig ... end
module ID : sig ... end
module Lit : sig ... end
module Clause : sig ... end
module Step_input : sig ... end
module Step_rup : sig ... end
module Step_bridge_lit_expr : sig ... end
module Step_cc : sig ... end
module Step_preprocess : sig ... end
module Step_clause_rw : sig ... end
module Step_unsat : sig ... end
module Step_proof_p1 : sig ... end
module Step_proof_r1 : sig ... end
module Step_bool_tauto : sig ... end
module Step_bool_c : sig ... end
module Step_true : sig ... end
module Fun_decl : sig ... end
module Expr_def : sig ... end
module Expr_bool : sig ... end
module Expr_if : sig ... end
module Expr_not : sig ... end
module Expr_eq : sig ... end
module Expr_app : sig ... end
module Expr_isa : sig ... end
module Step_view : sig ... end
module Step : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_quip/Proof/T/index.html b/dev/sidekick/Sidekick_quip/Proof/T/index.html index ca632e2e..25529ebc 100644 --- a/dev/sidekick/Sidekick_quip/Proof/T/index.html +++ b/dev/sidekick/Sidekick_quip/Proof/T/index.html @@ -1,2 +1,2 @@ -T (sidekick.Sidekick_quip.Proof.T)

Module Proof.T

Representation of terms, with explicit sharing

type t =
| Bool of bool
| App_fun of Fun.t * t array
| App_ho of t * t
| Ite of t * t * t
| Not of t
| Eq of t * t
| Ref of string
val view : t -> t
val equal : t -> t -> bool
val hash : t -> int
val true_ : t
val false_ : t
val bool : bool -> t
val not_ : t -> t
val eq : t -> t -> t
val ref : string -> t
val app_fun : Fun.t -> t array -> t
val const : Fun.t -> t
val app_ho : t -> t -> t
val ite : t -> t -> t -> t
\ No newline at end of file +T (sidekick.Sidekick_quip.Proof.T)

Module Proof.T

Representation of terms, with explicit sharing

type t =
| Bool of bool
| App_fun of Fun.t * t array
| App_ho of t * t
| Is_a of Fun.t * t
| Ite of t * t * t
| Not of t
| Eq of t * t
| Ref of string
val view : t -> t
val equal : t -> t -> bool
val hash : t -> int
val true_ : t
val false_ : t
val bool : bool -> t
val not_ : t -> t
val eq : t -> t -> t
val ref : string -> t
val app_fun : Fun.t -> t array -> t
val const : Fun.t -> t
val app_ho : t -> t -> t
val ite : t -> t -> t -> t
val is_a : Fun.t -> t -> t
\ No newline at end of file