koka-lang/madoko

INCLUDE code block within a linked list

catalin-hritcu opened this issue · 0 comments

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.