Zulip Chat Archive

Stream: general

Topic: representing math structures

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

Andrew Ashworth (Mar 05 2019 at 12:07):


Last updated: Aug 03 2023 at 10:10 UTC