The following warning says:
Warning: *-monoˡ-≤-nonNeg was deprecated in v2.0.
Please use *-monoˡ-≤-nonNeg instead.
It's wrong since it says you should use non-neg instead of non-neg. It is a warning on *-monoˡ-≤-pos, so I assume the warning should be:
Warning: *-monoˡ-≤-pos was deprecated in v2.0.
Please use *-monoˡ-≤-nonNeg instead.
I double-checked all other warnings in the Unnormalised/Properties.agda file and the rest seem good to me.
The following warning says:
It's wrong since it says you should use non-neg instead of non-neg. It is a warning on
*-monoˡ-≤-pos, so I assume the warning should be:I double-checked all other warnings in the
Unnormalised/Properties.agdafile and the rest seem good to me.