
  0 | module Scratchpad
  1 | 
  2 | import Data.Linear.Ref1
  3 | import Syntax.T1
  4 | 
  5 | %default total
  6 | 
  7 | fibo : Nat -> Nat
  8 | fibo n =
  9 |   run1 $ T1.do
 10 |      r1 <- ref1 (S Z)
 11 |      r2 <- ref1 (S Z)
 12 |      forN n (T1.do
 13 |        f1 <- read1 r1
 14 |        f2 <- read1 r2
 15 |        write1 r2 (f1 + f2)
 16 |        write1 r1 f2)
 17 |      read1 r1
 18 |