@@ -116,14 +116,14 @@ par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type
116116 -- is better in any case?
117117par (Delay x) = x
118118
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
120120||| x (which is typically a pattern argument)
121121||| @ x the larger value (typically a pattern argument)
122122||| @ y the smaller value (typically an argument to a recursive call)
123123assert_smaller : (x : a) -> (y : b) -> b
124124assert_smaller x y = y
125125
126−||| Assert to the totality checker than the given expression will always
126+||| Assert to the totality checker that the given expression will always
127127||| terminate.
128128assert_total : a -> a
129129assert_total x = x