[Agda] Definizione di semianello
Inviato: 10/07/2019, 23:33
Un semigruppo e un monoide si definiscono in Agda come segue:
Come si definisce, ora, un semianello? Questa definizione typechecka, ma non so (proprio a livello di sintassi) come specificare che l'operazione di monoide è \(\oplus\) e quella di semigruppo \(\circ\):
- Codice:
record Semigroup (a : Set) : Set where
field
_o_ : a → a → a
assoc : ∀ a b c → (a o b) o c ≡ a o (b o c)
record Monoid (a : Set) : Set where
field
semigroup : Semigroup a
open Semigroup semigroup
field
z : a
lId : ∀ x → z o x ≡ x
rId : ∀ x → x o z ≡ x
Come si definisce, ora, un semianello? Questa definizione typechecka, ma non so (proprio a livello di sintassi) come specificare che l'operazione di monoide è \(\oplus\) e quella di semigruppo \(\circ\):
- Codice:
record Semiring (a : Set) : Set where
field
monoid : Monoid a
semigroup : Semigroup a
field
_⊕_ : a → a → a
_o_ : a → a → a