Isabelle Theory Generation¶

Configuration¶

Enable Isabelle theory generation in front-matter:

---
preprocess:
  isabelle: true
---

To include theories at page bottom:

---
preprocess:
  isabelle: true
  isabelle_at_bottom: true
---

Including Generated Files¶

Include the generated Isabelle theory as a snippet using the !thy suffix:

--8<-- "docs/isabelle.juvix.md!thy:isabelle-add-def"

This provides the following output:

fun add :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat" where
  "add zero n = n" |
  "add (succ m) n = (succ (add m n))"