Which induction schemes (e.g. induction-recursion by Dybjer and Setzer, "Irish" induction-recursion by McBride or induction-induction by Forsberg and Setzer or perhaps some simpler ones) allow one to encode the following Agda definition
data A : Set where a : Maybe (List A) → A
I can think of some tricks to reformulate
List in this definition so that induction-recursion becomes applicable, but are there any schemes that would allow me to first say what a list is and then refer to this information to say what
A is the way it's done in Agda?
Edit: As follows from András Kovács's answer, this particular definition can be reformulated as an inductive family. Here is how to do it:
data Three : Set where one two three : Three data AG : Three → Set where a' : AG three → AG one nil' : AG two cons' : AG one → AG two → AG two nothing' : AG three just' : AG two → AG three A = AG one ListA = AG two MaybeListA = AG three a : MaybeListA → A a = a' nil : ListA nil = nil' cons : A → ListA → ListA cons = cons' nothing : MaybeListA nothing = nothing' just : ListA → MaybeListA just = just'