AltErgoLib.D_cnf
val make :
AltErgoLib.D_loop.DStd.Loc.file ->
Commands.sat_tdecl list ->
[< D_loop.Typer_Pipe.typechecked
| `Goal of Dolmen.Std.Expr.term
| `Check of Dolmen.Std.Expr.term list Hyp ]
D_loop.Typer_Pipe.stmt ->
Commands.sat_tdecl list
make acc stmt
Makes one or more Commands.sat_tdecl
from the type-checked statement stmt
and appends them to acc
.
val builtins :
Dolmen_loop.State.t ->
D_loop.Typer.lang ->
Dolmen_loop.Typer.T.builtin_symbols