package mc2

  1. Overview
  2. Docs

Source file Lemma.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

(** {1 Lemmas} *)

open Solver_types

type t = lemma
type view = lemma_view

let[@inline] pp out (l:t) = match l with
  | Lemma_bool_tauto -> Fmt.string out "bool_tauto"
  | Lemma_custom {view;tc} -> tc.tcl_pp out view

let tauto = Lemma_bool_tauto
let[@inline] make view tc: t = Lemma_custom {view;tc}

module TC = struct
  type t = tc_lemma

  let make ~pp () : t = { tcl_pp=pp }

end