You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{.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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: