Skip to content

Commit

Permalink
fix cost example to be more precise
Browse files Browse the repository at this point in the history
  • Loading branch information
dorchard committed Mar 8, 2024
1 parent f804cec commit 77f9d9d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion examples/cost.gr
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ two =
-- Prove (map f) in O(|f|n)

mapLinear : forall {a b : Type, n : Nat, f : Nat}
. (a -> b <f>) [] -> Vec n a -> (Vec n b) <n*f>
. (a -> b <f>) [n] -> Vec n a -> (Vec n b) <n*f>
mapLinear [_] Nil = pure Nil;
mapLinear [f] (Cons x xs) =
let y <- f x;
Expand Down

0 comments on commit 77f9d9d

Please sign in to comment.