Converter from HOAS to FOAS

fun conv (HAbs(f)) =

let val x = gensym ()

in Abs(x, conv (f (HSym(x))))

end

| conv (HApp(e1, e2)) = App(conv e1, conv e2)

| conv (HSym(s)) = Var(s)

Previous slide

Next slide

Back to first slide

View graphic version