sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page
module Bl : sig ... end
Boolean
module Bv : sig ... end
Bit-vector
module Rm : sig ... end
Rounding-mode
module Fp : sig ... end
Floating-point
module Ar : sig ... end
Array
module Uf : sig ... end
Uninterpreted function
const sort symbol
create a (first-order) constant of given sort with given symbol.
This creates a 0-arity function symbol.
val hash : 'a t -> int
hash t
compute the hash value for a term.
val pp : Format.formatter -> 'a term -> unit
pp formatter t
pretty print term.
type 'a view =
| Value : 'a value -> 'a view
| Const : 'a sort * string -> 'a view
| Var : [< bv | rm | fp ] as 'a sort -> 'a view
| Lambda : 'a variadic * 'b term -> ('a, 'b) fn view
| Equal : [< bv | rm | fp | ('b, 'c) ar ] as 'a term * 'a term -> bv view
| Distinct : [< bv | rm | fp | ('b, 'c) ar ] as 'a term * 'a term -> bv view
| Ite : bv term * [< bv | rm | fp | ('b, 'c) ar ] as 'a term * 'a term -> 'a view
| Bv : ('a, 'b) Bv.operator * 'b -> bv view
| Fp : ('a, 'b, 'c) Fp.operator * 'b -> 'c view
| Select : ('a, 'b) ar term * 'a term -> 'b view
| Store : ('a, 'b) ar term * 'a term * 'b term -> ('a, 'b) ar view
| Apply : ('a, 'b) fn term * 'a variadic -> 'b view
Algebraic view of formula terms.