Bug in HOL generation
With this input
open import Pervasives
type t = | Tapp of list t
type ast_t = | Ast_Tapp of list ast_t
let rec elab_t (Ast_Tapp ts) = let ts' = List.map elab_t ts in Tapp ts'
I get HOL output that includes:
val elab_t_defn = Hol_defn "elab_t" `
(elab_t (Ast_Tapp ts) = (let ts' = (\ . (MAP elab_t ts)) in Tapp ts'))`;
which is malformed.
This is on the most recent master branch checkout. This problem didn't seem to occur last night.