Theoria.Library.Nat (theoria v0.3.0)

Initial natural number declarations and primitive recursion.

Summary

env()

Returns a new environment extended with natural number declarations.

extend(env)

Extends an environment with natural number declarations.

inductive_spec()

Returns the inductive specification described by this library.

type()

The core universe for Type 0.

Returns a new environment extended with natural number declarations.

Extends an environment with natural number declarations.

Returns the inductive specification described by this library.

The core universe for Type 0.