Zulip Chat Archive

Stream: general

Topic: representing math structures


view this post on Zulip Minghao Liu (Mar 05 2019 at 06:49):

hello, has the Lean team considered using the "dependent record type with with construction" described in this paper "Dependently typed records for representing mathematical structure" to represent mathematical structures? The Agda technical report p85 mentioned this, but Agda decided to not use this

view this post on Zulip Andrew Ashworth (Mar 05 2019 at 12:07):

No?


Last updated: May 15 2021 at 02:11 UTC