[CakeML] Low-level Compiler Explorer

[Lars Hupel]

Dear list,

I'm currently trying to familiarize myself with CakeML. My current goal
is to generate ASTs inside Isabelle/HOL, and then continue to prove
certain properties wrt to the big step semantics.

What I'm struggling with at the moment are some fine points of how
certain terms should be represented as ASTs. For that, I wanted to play
a bit with the online Compiler Explorer. In the "AST" tab, it doesn't
really print an AST, but rather a pretty-printed version of the input.
However, I'm interested in a more low-level representation. Ideally, I
want to enter a recursive function and get out something like

  Dletrec [("foo", "xs", Fun "ys" ...)]

Is that at all possible?

Cheers
Lars