Define inductive branch with constraint on branch parameters

Using Coq
1

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

2

For an example how to define first-order logic in Coq and some best practices you could have a look at GitHub - uds-psl/coq-library-fol

1 Like