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 id l ~err ~k splits id (using split_id) into a list. If the list has a head s and a tail l, it tries and find in the list l a pair (s', indexed) such that s = s'. If the length of l matches the arity of indexed, the provided function is called, else err is called with s, the arity of indexed, and the lenght of l. If no match is found or the split list does not contain a head and a tail, k is called wiht the split list.

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; ..]