Theorem corpus for Theoria.Library.Bool.
These proofs document the initial boolean declarations and computation rules accepted by definitional equality.
Summary
Functions
Returns the unelaborated proof syntax for theorem bool_and_false_false.
Elaborates and checks theorem bool_and_false_false against the given environment.
Returns the unelaborated type syntax for theorem bool_and_false_false.
Returns the unelaborated proof syntax for theorem bool_and_false_true.
Elaborates and checks theorem bool_and_false_true against the given environment.
Returns the unelaborated type syntax for theorem bool_and_false_true.
Returns the unelaborated proof syntax for theorem bool_and_true_false.
Elaborates and checks theorem bool_and_true_false against the given environment.
Returns the unelaborated type syntax for theorem bool_and_true_false.
Returns the unelaborated proof syntax for theorem bool_and_true_left.
Elaborates and checks theorem bool_and_true_left against the given environment.
Returns the unelaborated type syntax for theorem bool_and_true_left.
Returns the unelaborated proof syntax for theorem bool_and_true_true.
Elaborates and checks theorem bool_and_true_true against the given environment.
Returns the unelaborated type syntax for theorem bool_and_true_true.
Returns the unelaborated proof syntax for theorem bool_not_false.
Elaborates and checks theorem bool_not_false against the given environment.
Returns the unelaborated type syntax for theorem bool_not_false.
Returns the unelaborated proof syntax for theorem bool_not_is_function.
Elaborates and checks theorem bool_not_is_function against the given environment.
Returns the unelaborated type syntax for theorem bool_not_is_function.
Returns the unelaborated proof syntax for theorem bool_not_true.
Elaborates and checks theorem bool_not_true against the given environment.
Returns the unelaborated type syntax for theorem bool_not_true.
Returns the unelaborated proof syntax for theorem bool_or_false_false.
Elaborates and checks theorem bool_or_false_false against the given environment.
Returns the unelaborated type syntax for theorem bool_or_false_false.
Returns the unelaborated proof syntax for theorem bool_or_false_left.
Elaborates and checks theorem bool_or_false_left against the given environment.
Returns the unelaborated type syntax for theorem bool_or_false_left.
Returns the unelaborated proof syntax for theorem bool_or_false_true.
Elaborates and checks theorem bool_or_false_true against the given environment.
Returns the unelaborated type syntax for theorem bool_or_false_true.
Returns the unelaborated proof syntax for theorem bool_or_true_false.
Elaborates and checks theorem bool_or_true_false against the given environment.
Returns the unelaborated type syntax for theorem bool_or_true_false.
Returns the unelaborated proof syntax for theorem bool_or_true_true.
Elaborates and checks theorem bool_or_true_true against the given environment.
Returns the unelaborated type syntax for theorem bool_or_true_true.
Returns the unelaborated proof syntax for theorem false_is_bool.
Elaborates and checks theorem false_is_bool against the given environment.
Returns the unelaborated type syntax for theorem false_is_bool.
Returns the unelaborated proof syntax for theorem true_is_bool.
Elaborates and checks theorem true_is_bool against the given environment.
Returns the unelaborated type syntax for theorem true_is_bool.
Functions
Returns the unelaborated proof syntax for theorem bool_and_false_false.
Elaborates and checks theorem bool_and_false_false against the given environment.
Returns the unelaborated type syntax for theorem bool_and_false_false.
Returns the unelaborated proof syntax for theorem bool_and_false_true.
Elaborates and checks theorem bool_and_false_true against the given environment.
Returns the unelaborated type syntax for theorem bool_and_false_true.
Returns the unelaborated proof syntax for theorem bool_and_true_false.
Elaborates and checks theorem bool_and_true_false against the given environment.
Returns the unelaborated type syntax for theorem bool_and_true_false.
Returns the unelaborated proof syntax for theorem bool_and_true_left.
Elaborates and checks theorem bool_and_true_left against the given environment.
Returns the unelaborated type syntax for theorem bool_and_true_left.
Returns the unelaborated proof syntax for theorem bool_and_true_true.
Elaborates and checks theorem bool_and_true_true against the given environment.
Returns the unelaborated type syntax for theorem bool_and_true_true.
Returns the unelaborated proof syntax for theorem bool_not_false.
Elaborates and checks theorem bool_not_false against the given environment.
Returns the unelaborated type syntax for theorem bool_not_false.
Returns the unelaborated proof syntax for theorem bool_not_is_function.
Elaborates and checks theorem bool_not_is_function against the given environment.
Returns the unelaborated type syntax for theorem bool_not_is_function.
Returns the unelaborated proof syntax for theorem bool_not_true.
Elaborates and checks theorem bool_not_true against the given environment.
Returns the unelaborated type syntax for theorem bool_not_true.
Returns the unelaborated proof syntax for theorem bool_or_false_false.
Elaborates and checks theorem bool_or_false_false against the given environment.
Returns the unelaborated type syntax for theorem bool_or_false_false.
Returns the unelaborated proof syntax for theorem bool_or_false_left.
Elaborates and checks theorem bool_or_false_left against the given environment.
Returns the unelaborated type syntax for theorem bool_or_false_left.
Returns the unelaborated proof syntax for theorem bool_or_false_true.
Elaborates and checks theorem bool_or_false_true against the given environment.
Returns the unelaborated type syntax for theorem bool_or_false_true.
Returns the unelaborated proof syntax for theorem bool_or_true_false.
Elaborates and checks theorem bool_or_true_false against the given environment.
Returns the unelaborated type syntax for theorem bool_or_true_false.
Returns the unelaborated proof syntax for theorem bool_or_true_true.
Elaborates and checks theorem bool_or_true_true against the given environment.
Returns the unelaborated type syntax for theorem bool_or_true_true.
Returns the unelaborated proof syntax for theorem false_is_bool.
Elaborates and checks theorem false_is_bool against the given environment.
Returns the unelaborated type syntax for theorem false_is_bool.
Returns the unelaborated proof syntax for theorem true_is_bool.
Elaborates and checks theorem true_is_bool against the given environment.
Returns the unelaborated type syntax for theorem true_is_bool.