Hello,
I am trying to define first-order logic terms with an inductive set.
Such terms include function applications which typically have the constraint that their arity must match the size of the argument list provided during the call of the function. I.e, I am trying to write this :
Inductive Term :=
| Var (name : string)
| FunApp (f: Function) (terms : list Term) (correct_size : arity f = length terms).
Unfortunaltely, I get the following error.
Non strictly positive occurrence of
"Term" in
"forall (f : Function) (terms : list Term),
arity f = Datatypes.length terms -> Term".
Is there a known workaround for cases like this?
Thanks a lot,
MRandl