untype transforms types, i.e. domains (dom-terms), exclusions (exc-terms), and sorts (``$''-terms) into active calls of the type/type1 builtin (which is only available in compiled RELFUN). Furthermore, expressions of the form expr : type and bnd[expr , expr ] are handled by transforming them into is-calls or type-calls.
The meaning of type(term, tterm), where tterm is either a dom-term, an exc-term, or an atom (denoting the name of a sort), is: if term is a variable, type it with tterm (i.e., fill the type slot of the GWAM representation of variables, ref-cells, with tterm), otherwise check if term is of type tterm.
The following examples show some of the cases covered by untype: