I've found HOAS to be a convenient notation for higher order functions in DSLs in Coq [1] and Python [2], but both use cases were to reason about lambda-calculu

I've found HOAS to be a convenient notation for higher order functions in DSLs in Coq [1] and Python [2], but both use cases were to reason about lambda-calculus. [1] https://github.com/fritzo/hstar/blob/6df3347/src/DeBruijn.v#L29 https://github.com/fritzo/hstar/blob/6df3347/src/DeBruijn.v#... [2] https://github.com/fritzo/pomagma/blob/ada575c/src/reducer/sugar.py#L14 https://github.com/fritzo/pomagma/blob/ada575c/src/reducer/s...