This tutorial consists of:

• ITree.Simple: simplified tutorial interface, available as a part of the library itself.

• Introduction.v: a detailed exposition of the core features.

• A case study with a small commented compiler from Imp to Asm:

  • Imp.v: The Imp language definition (a minimal imperative language from Software Foundations)
  • Asm.v: The Asm language definition (a control-flow-graph language)
  • AsmCombinators.v: High-level combinators for Asm
  • Imp2Asm.v: The compiler
  • Imp2AsmCorrectness.v: The correctness theorem (compile_correct).