The U Programming Language

u.txt

t_category my_term_category
v_category my_var_category

(* function i(x, y) *)
let i  = my_term_category "i" [_, _]

(* constant j *)
let j  = my_term_category "j" []

(* constant k *)
let k  = my_term_category "k" []

(* constant k' *)
let k' = my_term_category "k'" []

(* variable x *)
let x = my_var_category "x"

(* variable y *)
let y = my_var_category "y"

let my_order = (extended_order i >_ord j >_ord k >_ord k') +_ordset Std.default_order

let my_rule = rule (my_order) [(i x y, j); (j, k); (k, k')]

let my_term_system = completion (trsystem my_rule)