# Example:Inductive definition of string length

For example, we could define a function for computing the length of a string inductively:

Definition: len
Let be given inductively by and .

It is reasonable to use when defining because is a substructure of ; we must have already proved that before we prove that

We can then compute