{.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.
I can write code within a linked list like this:
However, if I try to import this code from a file, it doesn't work and breaks the layout of the entire slide:
Update: It's hard to write this here since GitHub interprets the markdown.