Issue #49 resolved

Bug in HOL generation

Scott Owens
created an issue

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' = 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.

Comments (1)

  1. Log in to comment