Gospel injects fs_apply symbols in the typed AST.

[n-osborne]

This issue has been raised offline by @mrjazzybread

This behaviour is observed when there is a function application where the term for the function is not a name.

For example, in this function definition:

(*@ function f (b : bool) : bool = (fun x -> x) b *)

Gospel type-checker will produce something like Tapp (fs_apply, [Tlambda ...; Tvar "b"]) for the body of the function.

In fact, it can't produce anything else in the current state of the typed AST as the application node (Tapp) in Tterm.term_node takes a lsymbol as its function argument.

We should make Tapp looks like:

  | Tapp of term * term list

and go from there.