Idris back end IRs

Idris' implementation has a number of intermediate languages that back end developers can use as a starting point. Quoting Edwin from IRC:

<edwinb> the data structures are in IRTS/ - I don't think they're that huge
<edwinb> IRTS/CodegenCommon.hs has the top level structure that contains all the 
         IRs
<edwinb> you've basically got LDecl, which is untyped lambda calculus, Decl,
         which is a first order language, and SDecl, which is ANF
<edwinb> more or less
<edwinb> oh, LDecl is lambda lifted too

Obviously this page wants expanding! For those new to them, lambda lifting and ANF both have tolerable wikipedia pages and are familiar to many functional compiler programmers, so it should be possible to find people to ask questions. Has anyone taken enough of a look at eg StackOverflow to know if there are good answers?

Idris-Compilation-Pipeline : https://github.com/idris-lang/Idris-dev/wiki/Idris-Compilation-Pipeline

Idris Compilation paper : https://eb.host.cs.st-andrews.ac.uk/drafts/compile-idris.pdf