Coq標準ライブラリの公理一覧

Coq-axiomlist.txt

Coq.Logic.ClassicalEpsilon.constructive_indefinite_description
Coq.Logic.ClassicalUniqueChoice.dependent_unique_choice
Coq.Logic.Classical_Prop.classic
Coq.Logic.Description.constructive_definite_description
Coq.Logic.Epsilon.epsilon_statement
Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq
Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
Coq.Logic.IndefiniteDescription.constructive_indefinite_description
Coq.Logic.JMeq.JMeq_eq
Coq.Logic.ProofIrrelevance.proof_irrelevance
Coq.Logic.RelationalChoice.relational_choice
Coq.Reals.Ranalysis_reg.AppVar
Coq.Reals.Raxioms.R1_neq_R0
Coq.Reals.Raxioms.Rinv_l
Coq.Reals.Raxioms.Rlt_asym
Coq.Reals.Raxioms.Rlt_trans
Coq.Reals.Raxioms.Rmult_1_l
Coq.Reals.Raxioms.Rmult_assoc
Coq.Reals.Raxioms.Rmult_comm
Coq.Reals.Raxioms.Rmult_lt_compat_l
Coq.Reals.Raxioms.Rmult_plus_distr_l
Coq.Reals.Raxioms.Rplus_0_l
Coq.Reals.Raxioms.Rplus_assoc
Coq.Reals.Raxioms.Rplus_comm
Coq.Reals.Raxioms.Rplus_lt_compat_l
Coq.Reals.Raxioms.Rplus_opp_r
Coq.Reals.Raxioms.archimed
Coq.Reals.Raxioms.completeness
Coq.Reals.Raxioms.total_order_T
Coq.Reals.Rdefinitions.R
Coq.Reals.Rdefinitions.R0
Coq.Reals.Rdefinitions.R1
Coq.Reals.Rdefinitions.Rinv
Coq.Reals.Rdefinitions.Rlt
Coq.Reals.Rdefinitions.Rmult
Coq.Reals.Rdefinitions.Ropp
Coq.Reals.Rdefinitions.Rplus
Coq.Reals.Rdefinitions.up
Coq.Sets.Ensembles.Extensionality_Ensembles