- (** tactic (params) = code *)
- | ETacticDefn of loc * tactic
- (** call goalname (params) etc. *)
- | ECallGoal of loc * id * expr list
- (** call *tactic (params) etc. *)
- | ETacticCtor of loc * id * expr list
- (** variable, or goal call with no parameters *)
+ (** goal (params) = patterns : exprs code *)
+ | EFuncDefn of loc * func
+ (** function (params) = code *)
+ | EPredDefn of loc * pred
+ (** predicate (params) = code *)
+ | ECall of loc * id * expr list
+ (** call goal (params) or function (params) *)
+ | EPredCtor of loc * id * expr list
+ (** constructor is-predicate (params) *)