simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor(core): add Proof_step

Browse source
This commit is contained in:
Simon Cruanes 2022-07-29 23:27:04 -04:00
parent a9ae790d7f
commit 7595f66e59
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
6 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/core/Sidekick_core.ml
View file

@ -25,6 +25,7 @@ end
module Bvar = Sidekick_core_logic.Bvar
module Lit = Lit
module Proof_step = Proof_step
module Proof_core = Proof_core
module Proof_sat = Proof_sat
module Proof_trace = Proof_trace

3
src/core/proof_step.ml Normal file
View file

@ -0,0 +1,3 @@
type id = int32
let pp = Fmt.int32

2
src/core/proof_term.ml
View file

@ -1,6 +1,6 @@
open Sidekick_core_logic
type step_id = int32
type step_id = Proof_step.id
type lit = Lit.t
type t = {

2
src/core/proof_term.mli
View file

@ -4,7 +4,7 @@
open Sidekick_core_logic
type step_id = int32
type step_id = Proof_step.id
type lit = Lit.t
type t = {

2
src/core/proof_trace.ml
View file

@ -1,5 +1,5 @@
type lit = Lit.t
type step_id = int32
type step_id = Proof_step.id
type proof_term = Proof_term.t
module Step_vec = struct

2
src/core/proof_trace.mli
View file

@ -10,7 +10,7 @@ open Sidekick_core_logic
type lit = Lit.t
type step_id = Proof_term.step_id
type step_id = Proof_step.id
(** Identifier for a tracing step (like a unique ID for a clause previously
added/proved) *)