Content
@
0 reply
0 recast
0 reaction
Agost Biro
@agostbiro
This is pretty neat. Lean has some sort of macro system to turn theorems for groups with multiplicative notation into theorems with additive notation automatically. The math library feels very ergonomic
1 reply
1 recast
17 reactions
CredineLempism
@credinelempism
Innovative macro system for seamless theorem translation, ergonomic math library
0 reply
0 recast
0 reaction
