Theoria.Library.Bool (theoria v0.7.0)

Initial computational boolean declarations.

This library introduces booleans as ordinary data in Type 0, distinct from the logical propositions True and False in Theoria.Library.Logic.

Summary

env()

Returns a new environment extended with boolean declarations.

extend(env)

Extends an environment with boolean declarations.

inductive_spec()

Returns the inductive specification described by this library.

type()

The core universe for Type 0.

Returns a new environment extended with boolean declarations.

Extends an environment with boolean declarations.

Returns the inductive specification described by this library.

The core universe for Type 0.