Zulip Chat Archive
Stream: general
Topic: declaring structures
Jakob von Raumer (Mar 10 2018 at 15:04):
Can I declare structures in the meta lang?
Sebastian Ullrich (Mar 10 2018 at 15:26):
meta structure? :)
Sebastian Ullrich (Mar 10 2018 at 15:27):
I guess you want to create one from a tactic. There's no such API yet.
Jakob von Raumer (Mar 11 2018 at 10:42):
How about for inductive?
Sebastian Ullrich (Mar 11 2018 at 10:49):
See https://groups.google.com/d/msg/lean-user/nmNlRiqogys/DKj97GkxAwAJ
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?
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: Dec 20 2023 at 11:08 UTC