INCLUDE code block within a linked list
catalin-hritcu opened this issue · 0 comments
catalin-hritcu commented
I can write code within a linked list like this:
- {.fragment} arbitrary total expression as decreases metric
val ackermann: m:nat -> n:nat -> Tot nat (decreases %[m;n]) let rec ackermann m n = if m = 0 then n + 1 else if n = 0 then ackermann (m - 1) 1 else ackermann (m - 1) (ackermann m (n - 1))
However, if I try to import this code from a file, it doesn't work and breaks the layout of the entire slide:
- {.fragment} arbitrary total expression as decreases metric
[INCLUDE=../../../code/pure-fun/Ackerman.fst]
Update: It's hard to write this here since GitHub interprets the markdown.