## Stream: general

### Topic: doc-gen quirks in bilin

#### Alex J. Best (Sep 19 2020 at 19:39):

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 (Sep 19 2020 at 19:40):

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 (Sep 19 2020 at 20:08):

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 (Sep 19 2020 at 20:10):

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 (Sep 19 2020 at 21:00):

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

#### Alex J. Best (Sep 20 2020 at 20:24):

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

Last updated: May 18 2021 at 16:25 UTC