Module Smyth.Term_gen
val fresh_ident : Lang.type_ctx -> char -> string
fresh_ident gamma c
returns an identifier starting with the characterc
that does not appear in the type contextgamma
val match_char : char
The canonical first character for variable names used in pattern matching in a
case
expression.
val clear_cache : unit -> unit
Clears the memoization cache. Important note: make sure to call
clear_cache
once synthesis is fully complete for a problem, and not any sooner or later!
val up_to_e : Lang.datatype_ctx -> int -> Lang.gen_goal -> Lang.exp Nondet.t
up_to_e sigma n goal
nondeterministically generates elimination forms at a goalgoal
up to (and including) AST sizen
.