Stream: math-comp users

Topic: ring_scope and nat notations


view this post on Zulip 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 *)

view this post on Zulip Cyril Cohen (Aug 19 2020 at 11:40):

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: Feb 08 2023 at 04:04 UTC