Zulip Chat Archive

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

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: Dec 20 2023 at 11:08 UTC