Stream: Lean Together 2021
Rob Lewis (Jan 05 2021 at 16:07):
Vaibhav has contributed two prerecorded talks: Axiomatic Geometry in Lean and Model Theory in Lean. These will become YouTube links when I have time, but we wanted to make them available ASAP. Ask him questions at tomorrow's social session!
Vaibhav Karve (Jan 05 2021 at 16:39):
Rob & Patrick, thank you once again for opportunity to speak! I am loving the conference. The only thing missing is the Pittsburg weather from last time :smile: :snowflake:
Aaron Anderson (Jan 05 2021 at 23:52):
I'm excited to see more model theory being done!
Aaron Anderson (Jan 05 2021 at 23:55):
I certainly find this definition of terms easier to read than the Flypitch definition - but without having worked in detail with either, I'm not sure what the technical advantages of one over the other are.
Aaron Anderson (Jan 06 2021 at 00:03):
Also - @Vaibhav Karve, you mentioned avoiding
fin n because the API is tricky. Are you aware of @Reid Barton's finvec PR? (#4406)
Aaron Anderson (Jan 06 2021 at 00:04):
Perhaps a more robust
finvec API would help - or maybe it'd just have the same nested inductive type issue as using
vector, I'm not sure.
Adam Topaz (Jan 06 2021 at 00:12):
@Vaibhav Karve very interesting!
Vaibhav Karve (Jan 06 2021 at 14:03):
@Aaron Anderson I had not seen that PR. Thanks for pointing that out. @Gabriel Ebner pointed out in one of the comments on that PR that
finvec will not result in nested induction. :tada: However, we will still need a strong API for
finvec in order to make it work.
Last updated: May 08 2021 at 22:13 UTC