mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 19:55:41 -05:00
reexport more types in Term
This commit is contained in:
parent
e1717f3afe
commit
9e52183b45
2 changed files with 24 additions and 2 deletions
|
|
@ -1,7 +1,18 @@
|
||||||
|
|
||||||
open Solver_types
|
open Solver_types
|
||||||
|
|
||||||
type t = term
|
type t = term = {
|
||||||
|
mutable term_id : int;
|
||||||
|
mutable term_ty : ty;
|
||||||
|
term_cell : t term_cell;
|
||||||
|
}
|
||||||
|
|
||||||
|
type 'a cell = 'a term_cell =
|
||||||
|
| Bool of bool
|
||||||
|
| App_cst of cst * 'a IArray.t
|
||||||
|
| If of 'a * 'a * 'a
|
||||||
|
| Case of 'a * 'a ID.Map.t
|
||||||
|
| Custom of { view : 'a term_view_custom; tc : term_view_tc; }
|
||||||
|
|
||||||
type 'a custom = 'a Solver_types.term_view_custom = ..
|
type 'a custom = 'a Solver_types.term_view_custom = ..
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,18 @@
|
||||||
|
|
||||||
open Solver_types
|
open Solver_types
|
||||||
|
|
||||||
type t = term
|
type t = term = {
|
||||||
|
mutable term_id : int;
|
||||||
|
mutable term_ty : ty;
|
||||||
|
term_cell : t term_cell;
|
||||||
|
}
|
||||||
|
|
||||||
|
type 'a cell = 'a term_cell =
|
||||||
|
| Bool of bool
|
||||||
|
| App_cst of cst * 'a IArray.t
|
||||||
|
| If of 'a * 'a * 'a
|
||||||
|
| Case of 'a * 'a ID.Map.t
|
||||||
|
| Custom of { view : 'a term_view_custom; tc : term_view_tc; }
|
||||||
|
|
||||||
type 'a custom = 'a Solver_types.term_view_custom = ..
|
type 'a custom = 'a Solver_types.term_view_custom = ..
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue