@@ -116,14 +116,14 @@ par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type
116 -- is better in any case?
116 -- is better in any case?
117par (Delay x) = x
117par (Delay x) = x
119−||| Assert to the totality checker than y is always structurally smaller than
119+||| Assert to the totality checker that y is always structurally smaller than
120||| x (which is typically a pattern argument)
120||| x (which is typically a pattern argument)
121||| @ x the larger value (typically a pattern argument)
121||| @ x the larger value (typically a pattern argument)
122||| @ y the smaller value (typically an argument to a recursive call)
122||| @ y the smaller value (typically an argument to a recursive call)
123assert_smaller : (x : a) -> (y : b) -> b
123assert_smaller : (x : a) -> (y : b) -> b
124assert_smaller x y = y
124assert_smaller x y = y
126−||| Assert to the totality checker than the given expression will always
126+||| Assert to the totality checker that the given expression will always
127||| terminate.
127||| terminate.
128assert_total : a -> a
128assert_total : a -> a
129assert_total x = x
129assert_total x = x