Theoria.Library.List (theoria v0.3.0)

Copy Markdown View Source

Initial polymorphic list declarations and primitive recursion.

Summary

Functions

Returns a new Nat environment extended with list declarations.

Extends an environment with list declarations. Requires Nat declarations.

Returns the inductive specification described by this library.

Functions

env()

Returns a new Nat environment extended with list declarations.

extend(env)

Extends an environment with list declarations. Requires Nat declarations.

inductive_spec()

Returns the inductive specification described by this library.