module Unroll: sig
.. end
Unrolling of (Co)inductive Predicates
type
term = Nunchaku_core.TermInner.Default.t
type
decode_state
val name : string
val unroll : (term, term) Nunchaku_core.Problem.t ->
(term, term) Nunchaku_core.Problem.t * decode_state
val decode_model : state:decode_state ->
(term, term) Nunchaku_core.Model.t ->
(term, term) Nunchaku_core.Model.t
val pipe : print:bool ->
check:bool ->
((term, term) Nunchaku_core.Problem.t,
(term, term) Nunchaku_core.Problem.t,
(term, term) Nunchaku_core.Problem.Res.t,
(term, term) Nunchaku_core.Problem.Res.t)
Nunchaku_core.Transform.t
Pipeline component
val pipe_with : ?on_decoded:('d -> unit) list ->
decode:(decode_state -> 'c -> 'd) ->
print:bool ->
check:bool ->
((term, term) Nunchaku_core.Problem.t,
(term, term) Nunchaku_core.Problem.t, 'c, 'd)
Nunchaku_core.Transform.t
Generic Pipe Component