Module `Smyth.Exp`

val syntactically_equal : Lang.exp -> Lang.exp -> bool: syntactically_equal e1 e2 determines if e1 and e2 have the same abstract syntax tree.

val largest_hole : Lang.exp -> Lang.hole_name: largest_hole e returns the greatest-numbered hole in e

val has_special_recursion : Lang.exp -> bool: has_special_recursion e determines if e or one of its subexpressions has an application marked as "special". See Lang.exp for details about "special" applications.

val fill_hole : (Lang.hole_name * Lang.exp) -> Lang.exp -> Lang.exp: fill_hole (h, e) root replaces a hole ??_h with the expression e in the expression root.