search

math-comp / math-comp

Mathematical Components
https://math-comp.github.io
583 stars 113 forks source link

Should `f \min g` and `f \max g` notations be defined in `function_scope` ? #978

Open pi8027 opened 1 year ago

pi8027 commented 1 year ago

https://github.com/math-comp/math-comp/blob/082c28dc6562c3d947d52b74bd2a6bb592941562/mathcomp/ssreflect/order.v#L1265-L1266 It also seems to apply here: https://github.com/math-comp/math-comp/blob/082c28dc6562c3d947d52b74bd2a6bb592941562/mathcomp/algebra/ssralg.v#L6203-L6210

pi8027 commented 1 year ago

I thought that the point of fun_scope is to locally increase the priority of the notations defined in fun_scope in a context where a function is expected, e.g., the third argument of map. However, many of them actually have function_scope defined in the Coq standard library.

About map.
map : forall {T1 T2 : Type}, (T1 -> T2) -> seq T1 -> seq T2

map is not universe polymorphic
Arguments map {T1 T2}%type_scope f%function_scope s%seq_scope
                                   ^^^^^^^^^^^^^^
map is transparent
Expands to: Constant mathcomp.ssreflect.seq.map

Shouldn't we declare Bind Scope fun_scope with Funclass. to fix it, or even deprecate fun_scope and replace it with function_scope to unify them?

pi8027 commented 9 months ago

https://github.com/math-comp/math-comp/pull/1145#issuecomment-1895355450