package jasmin

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module GRing.Builders_211

val coq_Builders_211_R__canonical__GRing_Zmodule : 'a1 Coq_isNmodule.axioms_ -> 'a1 Choice.Coq_hasChoice.axioms_ -> 'a1 Eqtype.Coq_hasDecEq.axioms_ -> 'a1 Nmodule_isZmodule.axioms_ -> Zmodule.coq_type
val coq_GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing : 'a1 Coq_isNmodule.axioms_ -> 'a1 Choice.Coq_hasChoice.axioms_ -> 'a1 Eqtype.Coq_hasDecEq.axioms_ -> 'a1 Nmodule_isZmodule.axioms_ -> ('a1, 'a1) Zmodule_isComRing.phant_axioms -> 'a1 Nmodule_isSemiRing.axioms_
val coq_Builders_211_R__canonical__GRing_SemiRing : 'a1 Coq_isNmodule.axioms_ -> 'a1 Choice.Coq_hasChoice.axioms_ -> 'a1 Eqtype.Coq_hasDecEq.axioms_ -> 'a1 Nmodule_isZmodule.axioms_ -> ('a1, 'a1) Zmodule_isComRing.phant_axioms -> SemiRing.coq_type
val coq_GRing_Zmodule_isComRing__to__GRing_SemiRing_hasCommutativeMul : 'a1 Coq_isNmodule.axioms_ -> 'a1 Choice.Coq_hasChoice.axioms_ -> 'a1 Eqtype.Coq_hasDecEq.axioms_ -> 'a1 Nmodule_isZmodule.axioms_ -> ('a1, 'a1) Zmodule_isComRing.phant_axioms -> 'a1 SemiRing_hasCommutativeMul.axioms_