The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Here it is:

Inductive list A: nat → Type :=

 | nil: list A 0

 | cons: ∀ n, A → list A n → list A (S n).

Definition Language (A B: Type) := A → nat.

Inductive Term A B (W: Language A B) :=

 | variable: nat → Term W

 | function_node: ∀ x, list (Term W) (W x) → Term W

 | binder_node: ∀ (b: B) (v: nat), Term W → Term W.

 

Here I want to add the following condition in this inductive definition (for binder_node case).
 

Fixpoint variable_is_free A B (W: Language A B) (T: Term W) (x: nat) :=

 match T with

 | variable _ v => True

 | function_node _ L => Forall L (λ t, variable_is_free t x)

 | binder_node _ v t => v <> x ∧ variable_is_free t x

 end.

It should be something similar to this:
 

Inductive Term A B (W: Language A B) :=

 | variable: nat → Term W

 | function_node: ∀ x, list (Term W) (W x) → Term W

 | binder_node: ∀ (b: B) (v: nat) (T: Term W), variable_is_free T v → Term W

with variable_is_free A B (W: Language A B) := ...

 

How can I do such thing?