doc-gen quirks in bilin

Stream: general

[Alex J. Best]

On docs#bilin_form the declarations have this random c appearing before the bilin in bilin_add_left i.e.

structure bilin_form (R : Type u) (M : Type v) [ring R] [add_comm_group M] [module R M] :
Type (max u v)
(bilin : M → M → R)
(bilin_add_left : ∀ (x y z : M), c.bilin (x + y) z = c.bilin x z + c.bilin y z)
(bilin_smul_left : ∀ (a : R) (x y : M), c.bilin (a • x) y = a * c.bilin x y)
(bilin_add_right : ∀ (x y z : M), c.bilin x (y + z) = c.bilin x y + c.bilin x z)
(bilin_smul_right : ∀ (a : R) (x y : M), c.bilin x (a • y) = a * c.bilin x y)

is this necessary or some artifact of the doc-gen process, or the source?

[Alex J. Best]

Also the brackets surrounding structure fields being defined by css means that they dont get copy pasted, should we invest effort into making the doc declarations copy-pastable?

[Alex J. Best]

If I print the actual definition in lean I see

bilin_form.bilin_add_left : ∀ {R : Type u} {M : Type v} [_inst_1 : ring R] [_inst_2 : add_comm_group M] [_inst_3 : module R M]
(c : bilin_form R M) (x y z : M), c.bilin (x + y) z = c.bilin x z + c.bilin y z
b

so the c is an explicit argument in the generated equation.

[Alex J. Best]

So the question is should doc-gen conform to the source code and not have c. or the output of #print and include (c : bilin_form R M). Leaving it as is seems like it could get confusing to me.

[Bryan Gin-ge Chen]

Good catch. Do you mind creating issues for both of these?

[Alex J. Best]

Done, doc-gen#67 and doc-gen#68.