Noop builtins function.

A convenient function for merging a list of builtin parser functions into a single builtin function.

The type of indexed family of operators.

parse_id basename indexes f ~err ~k uses the function f to get an expected arity for the indexed identifier, and then tries and parse the index list according to the returned specification.

Suitable err function for parse_id for typing sort indexed families.

Suitable err function for parse_id for typing term indexed families.

make_op (module Type) env ast op arity args ret checks that args is the empty list and returns Some (ret ()), else it raises the appropriate exception from the typechecking module.

Same as make_op0 but the returning function takes a term as argument.

Same as make_op0 but the returning function takes a couple of terms as argument.

Same as make_op0 but the returning function takes a triple of terms as argument.

Same as make_op0 but the returning function takes a quadruple of terms as argument.

Same as make_op0 but takes an arity first, and the returning function takes a list of terms as argument. The list is guaranteed to have the same length as the given arity.

Ensures the list of arguments is at least of size 2 (used for associative symbols).

Fold application of a left-associative function on a list.

• raises Invalid_argument

  if the list is empty.

Fold application of a right-associative function on a list.

• raises Invalid_argument

  if the list is empty.

Ensures the list of arguments is at least of size 2 (used for chainable symbols).

Map a function on succesive pairs of elements in the arguments lists, and build the resulting conjunction. map_chain (module Type) mk [t1; t2; ..; tn] is Type.T._and [mk t1 t2; mk t2 t3; ..]