WIP: new datatype compiler

[cipher1024]

---

The goal of this PR is to enable the specification of inductive and coinductive data types using syntax such as

data tree (a : Type) 
| tip : tree
| node : a -> tree -> tree -> tree

codata inf_tree (a b : Type)
| node : a -> (b -> inf_tree) -> inf_tree

and have the relevant recursors and corecursors generated appropriately. The current infrastructure does not support nesting but it is a planned extension.

[digama0]

This should be in the tactic or meta namespace.

[digama0]

@cipher1024 Could you get this PR compiling? I can try applying some fixes directly but I can't even begin to understand the code until everything is working as intended.

[cipher1024]

That's a fair point. This version attempts to generate a specialized liftp and that's what's broken. I'm going to take that out and that should work. When #3915 finally gets merged, I'll add some properties to test the parts better and of course more documentation.

[digama0]

@cipher1024 Have you looked at the error message? I think it's much more basic than that - data.qpf.compiler.fn_var references tactic.mk_has_to_format which doesn't exist.

[cipher1024]

Oh, I must have forgotten to commit that file. Thanks! I didn't look closely at the failure because I knew there were more errors.

[YaelDillies]

It is highly unlikely that this will happen in Lean 3. Let's revisit after the port.