Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

INCLUDE code block within a linked list #61

Open
catalin-hritcu opened this issue Jul 1, 2019 · 0 comments
Open

INCLUDE code block within a linked list #61

catalin-hritcu opened this issue Jul 1, 2019 · 0 comments

Comments

@catalin-hritcu
Copy link

catalin-hritcu commented Jul 1, 2019

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant