Zulip Chat Archive

Stream: general

Topic: add_inductive

Jakob von Raumer (Mar 21 2018 at 13:42):

Why does

tactic.add_inductive `foo [] 0 `(Type) $
[(`mk, expr.pi `mk binder_info.default (expr.app (expr.const `list [level.zero]) (expr.const `foo [])) (expr.const `foo []))],

fail?

Sebastian Ullrich (Mar 21 2018 at 13:46):

That's a nested inductive type, add_inductive only supports basic inductive types

Jakob von Raumer (Mar 21 2018 at 13:47):

Too bad, and there's no API for the nested ones, right?

Sebastian Ullrich (Mar 21 2018 at 13:48):

Right

Jakob von Raumer (Mar 21 2018 at 13:50):

But are they internally reduced to basic inductive types?

Kevin Buzzard (Mar 21 2018 at 13:53):

That's what is claimed in section 7.9 of TPIL : https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#mutual-and-nested-inductive-types

Sebastian Ullrich (Mar 21 2018 at 13:53):

Yes https://github.com/leanprover/lean/wiki/Compiling-nested-inductive-types

Jakob von Raumer (Mar 21 2018 at 13:54):

Nice, thanks!

Jakob von Raumer (Mar 21 2018 at 13:58):

This is done in C++ but outside the kernel, right?

Mario Carneiro (Mar 21 2018 at 13:58):

yes

Jakob von Raumer (Mar 21 2018 at 13:59):

Why isn't it done in Lean?

Mario Carneiro (Mar 21 2018 at 14:01):

It could be...

Mario Carneiro (Mar 21 2018 at 14:02):

I started working on that a while back, but then the ground started shaking and I decided to wait for the dust to settle

Moses Schönfinkel (Mar 21 2018 at 14:12):

Very poetic!

Last updated: Dec 20 2023 at 11:08 UTC