What's a better (more generalisable and robust) way of writing `view`

in the following? I'd like to be able to deal with arbitrary-ary choices of constructors and preferably constructors with an arbitrary number of arguments.

```
Variable A B C D : Type.
Variant View : (A + (Empty_set + B)) + (C + D) -> Type :=
| view0 : forall x, View (inl (inl x))
| view1 : forall x, View (inl (inr (inr x)))
| view2 : forall x, View (inr (inl x))
| view3 : forall x, View (inr (inr x)).
Lemma view x : View x.
Proof.
repeat destruct x as [x|x]; try econstructor; destruct x.
Defined.
```

you can use match goal, and match hypotheses by type, to find what to destruct. For construction I’d recommend eauto + Local Hint Constructors (with a separate hint db). But doing any of this in Defined is… somewhat dangerous.

(but I guess you know the last bit)

Haven't used it myself but maybe Elpi could be nicer? We use it for metaprogramming

Thanks for the hints! I'll try them out tomorrow.

Maybe if I'm doing more than a one-liner, I can do something better and more general. What sort of information can I get about types, in Elpi or otherwise? For example, I'd like to be able to tell whether a given type normalises to a `Variant`

or `Record`

, and not an `Inductive`

(to avoid infinitely destructing `nat`

s, for example).

Under the disclaimer that I don't get exactly what you are trying to do ;-) all the info about Elpi is on its website, including tutorials.

The APIs you way use are probably these and that one where you can query if an inductive is a recursive type and all its info.

You also have APIs for reducing a term, or typing it.

Last updated: Oct 03 2023 at 20:01 UTC