Nuprl Definition : rng_sig
RngSig ==
car:Type
× eq:car ⟶ car ⟶ 𝔹
× le:car ⟶ car ⟶ 𝔹
× plus:car ⟶ car ⟶ car
× zero:car
× minus:car ⟶ car
× times:car ⟶ car ⟶ car
× one:car
× (car ⟶ car ⟶ (car?))
Definitions occuring in Statement :
bool: 𝔹,
unit: Unit,
function: x:A ⟶ B[x],
product: x:A × B[x],
union: left + right,
universe: Type
Definitions occuring in definition :
universe: Type,
bool: 𝔹,
product: x:A × B[x],
function: x:A ⟶ B[x],
union: left + right,
unit: Unit
Latex:
RngSig ==
car:Type
\mtimes{} eq:car {}\mrightarrow{} car {}\mrightarrow{} \mBbbB{}
\mtimes{} le:car {}\mrightarrow{} car {}\mrightarrow{} \mBbbB{}
\mtimes{} plus:car {}\mrightarrow{} car {}\mrightarrow{} car
\mtimes{} zero:car
\mtimes{} minus:car {}\mrightarrow{} car
\mtimes{} times:car {}\mrightarrow{} car {}\mrightarrow{} car
\mtimes{} one:car
\mtimes{} (car {}\mrightarrow{} car {}\mrightarrow{} (car?))
Date html generated:
2016_05_15-PM-00_19_58
Last ObjectModification:
2015_09_23-AM-06_25_29
Theory : rings_1
Home
Index