bug.timl

structure Bug = struct
open Basic
open List
       
absidx T_fun1 : BigO (fn m n => $m * $n) with
fun fun1 ['a] {m n : Nat} (le : 'a * 'a -- $m --> bool) (l : list 'a {n}) return unit using T_fun1 m n =
  ()
end
 
(* absidx T_fun2 : BigO (fn m n => $m * $n) with *)
absidx T_fun2 : BigO (fn m n => $m * $n) = fn m n => T_fun1 m (n-1) + 2.0
fun fun2 ['a] {m n : Nat} (le : 'a * 'a -- $m --> bool) (l : list 'a {n}) return unit using T_fun2 m n =
  case l of
      [] => ()
    | hd :: tl =>
      let
          val () = fun1 le tl
      in
          ()
      end
(* end *)

end