Theoria.Library.Equality.Theorems (theoria v0.3.0)

Theorem corpus for primitive propositional equality.

Summary

Functions

eq_congr_proof()

Returns the unelaborated proof syntax for theorem eq_congr.

eq_congr_theorem(env \\ Theoria.new_env())

Elaborates and checks theorem eq_congr against the given environment.

eq_congr_type()

Returns the unelaborated type syntax for theorem eq_congr.

eq_ndrec_proof()

Returns the unelaborated proof syntax for theorem eq_ndrec.

eq_ndrec_theorem(env \\ Theoria.new_env())

Elaborates and checks theorem eq_ndrec against the given environment.

eq_ndrec_type()

Returns the unelaborated type syntax for theorem eq_ndrec.

eq_refl_proof()

Returns the unelaborated proof syntax for theorem eq_refl.

eq_refl_theorem(env \\ Theoria.new_env())

Elaborates and checks theorem eq_refl against the given environment.

eq_refl_type()

Returns the unelaborated type syntax for theorem eq_refl.

eq_subst_proof()

Returns the unelaborated proof syntax for theorem eq_subst.

eq_subst_theorem(env \\ Theoria.new_env())

Elaborates and checks theorem eq_subst against the given environment.

eq_subst_type()

Returns the unelaborated type syntax for theorem eq_subst.

eq_symm_proof()

Returns the unelaborated proof syntax for theorem eq_symm.

eq_symm_theorem(env \\ Theoria.new_env())

Elaborates and checks theorem eq_symm against the given environment.

eq_symm_type()

Returns the unelaborated type syntax for theorem eq_symm.

eq_trans_proof()

Returns the unelaborated proof syntax for theorem eq_trans.

eq_trans_theorem(env \\ Theoria.new_env())

Elaborates and checks theorem eq_trans against the given environment.

eq_trans_type()

Returns the unelaborated type syntax for theorem eq_trans.