@@ -524,7 +524,10 @@ data LikeNat = LikeZ | LikeS
525isLikeNat :: IState -> Name -> Maybe LikeNat
525isLikeNat :: IState -> Name -> Maybe LikeNat
526isLikeNat ist cn
526isLikeNat ist cn
527+ -- Nat itself is special-cased in Idris/DataOpts.hs,
528+ -- which will have already happened at this point.
527− -- if the optimisation is disabled then nothing looks like Nat
530+ -- If the optimisation is disabled then nothing looks like Nat.
528 | GeneralisedNatHack `notElem` opt_optimise (idris_options ist)
531 | GeneralisedNatHack `notElem` opt_optimise (idris_options ist)
529 = Nothing
532 = Nothing