Ssreflect Users Discussion List

[Frédéric Chyzak <>]

Reading the header of ssrfun.v makes me have the following questions:

1. I understand the name oapp, but not odflt, obind, and omap.  What is the 
intuition behind those names?

2. Where is the meaning of Variables sufficiently described to compare the 
definitions of pcancel and ocancel:

Variables (rT aT : Type) (f : aT -> rT).

Definition pcancel g := forall x, g (f x) = Some x.

Definition ocancel (g : aT -> option rT) h := forall x, oapp h x (g x) = x.

The signatures of these constants (as obtained by About) suggest me that 
variables declared by Variables are added to the signature of the definition 
if 
they explicitly appear or are made necessary by type inference.  Is this 
right?

Is this the wanted behaviour?

3. I tried to understand the proof of can_pcan (to try and clarify the 
implicit nature of f in some but not all definitions).  Seemingly, the source 
type of f is counter-intuitively named x, which in the beginning of the file 
is 
rather the variable at which f is applied.

Frédéric