Karl Palmskog (Aug 19 2020 at 10:55): Karl Palmskog (Aug 19 2020 at 10:55):whenever I require-open ssralg and ssrnum and open ring_scope, my usual nat notations stop working. Is there a way to make them work again? For example:
From mathcomp.ssreflect Require Import all_ssreflect.
From mathcomp.algebra Require Import ssralg ssrnum.
Check 1%nat < 1.
Open Scope ring_scope.
Fail Check 1%nat < 1. (* The term "1" has type "nat" while it is expected to have type "Order.POrder.sort ?T". *)
Check (1 < 1)%nat. (* Works but annoying *)
First, we use %N instead of %nat .
Since mathcomp 1.11, you should always import order whenever you import ssrnum, otherwise you might be missing tons of important canonical structures! As soon as you do this you should be able to write 1%N < 1%N for example (not 1%N < 1, because the second 1 would be Ring.one), but I recommend you use (1 < 1)%N instead in order to use leq rather than Order.lt to be able to rewrite with theorems from ssrnat. Unfortunately, Coq notation system works top down (an argument of a notation/definition can be tagged in some scope), and not bottom up (the type / scope information of a given object cannot be used to determine the scope of a surrounding notation), and there is no way to get around this to my knowledge...
Last updated: Apr 19 2024 at 08:01 UTC