ϵ">]>
[CL] Structural case analysis on lists. Syntax:
Example(s):
where and are new variables (eigen-variables).
The predicate is defined in the module Standard.
[CL] Structural induction on lists. Syntax:
where the induction formula is formed from the current sequent.
Example(s):
The predicate is defined in the module Standard.
List concatenation. The list concatenation function , written as x++y, is defined in the module and the following properties are built in into the CL theorem prover:
We write as an abbreviation for .