Theorem corpus for Theoria.Library.Logic.
These proofs cover the initial logical declarations for implication-like
function types, false elimination, negation, and conjunction. They exercise
the public theorem DSL against both Theoria.Library.Logic.env/0 and the
standard Theoria.Prelude.env/0.
Summary
Functions
Returns the unelaborated proof syntax for theorem and_assoc_left.
Elaborates and checks theorem and_assoc_left against the given environment.
Returns the unelaborated type syntax for theorem and_assoc_left.
Returns the unelaborated proof syntax for theorem and_assoc_right.
Elaborates and checks theorem and_assoc_right against the given environment.
Returns the unelaborated type syntax for theorem and_assoc_right.
Returns the unelaborated proof syntax for theorem and_comm.
Elaborates and checks theorem and_comm against the given environment.
Returns the unelaborated type syntax for theorem and_comm.
Returns the unelaborated proof syntax for theorem and_intro_eta.
Elaborates and checks theorem and_intro_eta against the given environment.
Returns the unelaborated type syntax for theorem and_intro_eta.
Returns the unelaborated proof syntax for theorem and_left_eta.
Elaborates and checks theorem and_left_eta against the given environment.
Returns the unelaborated type syntax for theorem and_left_eta.
Returns the unelaborated proof syntax for theorem and_right_eta.
Elaborates and checks theorem and_right_eta against the given environment.
Returns the unelaborated type syntax for theorem and_right_eta.
Returns the unelaborated proof syntax for theorem const.
Elaborates and checks theorem const against the given environment.
Returns the unelaborated type syntax for theorem const.
Returns the unelaborated proof syntax for theorem contradiction.
Elaborates and checks theorem contradiction against the given environment.
Returns the unelaborated type syntax for theorem contradiction.
Returns the unelaborated proof syntax for theorem double_negation_intro.
Elaborates and checks theorem double_negation_intro against the given environment.
Returns the unelaborated type syntax for theorem double_negation_intro.
Returns the unelaborated proof syntax for theorem false_elim_eta.
Elaborates and checks theorem false_elim_eta against the given environment.
Returns the unelaborated type syntax for theorem false_elim_eta.
Returns the unelaborated proof syntax for theorem identity.
Elaborates and checks theorem identity against the given environment.
Returns the unelaborated type syntax for theorem identity.
Returns the unelaborated proof syntax for theorem not_false.
Elaborates and checks theorem not_false against the given environment.
Returns the unelaborated type syntax for theorem not_false.
Functions
Returns the unelaborated proof syntax for theorem and_assoc_left.
Elaborates and checks theorem and_assoc_left against the given environment.
Returns the unelaborated type syntax for theorem and_assoc_left.
Returns the unelaborated proof syntax for theorem and_assoc_right.
Elaborates and checks theorem and_assoc_right against the given environment.
Returns the unelaborated type syntax for theorem and_assoc_right.
Returns the unelaborated proof syntax for theorem and_comm.
Elaborates and checks theorem and_comm against the given environment.
Returns the unelaborated type syntax for theorem and_comm.
Returns the unelaborated proof syntax for theorem and_intro_eta.
Elaborates and checks theorem and_intro_eta against the given environment.
Returns the unelaborated type syntax for theorem and_intro_eta.
Returns the unelaborated proof syntax for theorem and_left_eta.
Elaborates and checks theorem and_left_eta against the given environment.
Returns the unelaborated type syntax for theorem and_left_eta.
Returns the unelaborated proof syntax for theorem and_right_eta.
Elaborates and checks theorem and_right_eta against the given environment.
Returns the unelaborated type syntax for theorem and_right_eta.
Returns the unelaborated proof syntax for theorem const.
Elaborates and checks theorem const against the given environment.
Returns the unelaborated type syntax for theorem const.
Returns the unelaborated proof syntax for theorem contradiction.
Elaborates and checks theorem contradiction against the given environment.
Returns the unelaborated type syntax for theorem contradiction.
Returns the unelaborated proof syntax for theorem double_negation_intro.
Elaborates and checks theorem double_negation_intro against the given environment.
Returns the unelaborated type syntax for theorem double_negation_intro.
Returns the unelaborated proof syntax for theorem false_elim_eta.
Elaborates and checks theorem false_elim_eta against the given environment.
Returns the unelaborated type syntax for theorem false_elim_eta.
Returns the unelaborated proof syntax for theorem identity.
Elaborates and checks theorem identity against the given environment.
Returns the unelaborated type syntax for theorem identity.
Returns the unelaborated proof syntax for theorem not_false.
Elaborates and checks theorem not_false against the given environment.
Returns the unelaborated type syntax for theorem not_false.