Zulip Chat Archive

Stream: general

Topic: declaring structures


view this post on Zulip Jakob von Raumer (Mar 10 2018 at 15:04):

Can I declare structures in the meta lang?

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 15:26):

meta structure? :)

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 15:27):

I guess you want to create one from a tactic. There's no such API yet.

view this post on Zulip Jakob von Raumer (Mar 11 2018 at 10:42):

How about for inductive?

view this post on Zulip Sebastian Ullrich (Mar 11 2018 at 10:49):

See https://groups.google.com/d/msg/lean-user/nmNlRiqogys/DKj97GkxAwAJ

view this post on Zulip Jakob von Raumer (Mar 11 2018 at 11:12):

But that doesn't mean that using environment.add_inductive will render the type completely useless, right?

view this post on Zulip Sebastian Ullrich (Mar 11 2018 at 12:22):

It's useless to end users, but not useless to other meta programs like the coinductive predicates


Last updated: May 14 2021 at 22:15 UTC