affeldt-aist / monae

Monadic effects and equational reasonig in Coq
GNU Lesser General Public License v2.1
68 stars 12 forks source link

Clarify eqtype #118

Closed garrigue closed 1 year ago

garrigue commented 1 year ago

Clearer definition and naming of computable equality axioms comparablePc and eqPc in monae_lib.