File: V1.v

package info (click to toggle)
coq-hierarchy-builder 1.4.0-2
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 1,632 kB
  • sloc: ml: 159; makefile: 104
file content (15 lines) | stat: -rw-r--r-- 498 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
 
Require Import ZArith ssreflect ssrfun.
From HB Require Import structures.

HB.mixin Record is_monoid (M : Type) := {
  zero  : M;
  add   : M -> M -> M;
  addrA : associative add; (* add is associative. *)
  add0r : forall x, add zero x = x; (* zero is neutral *)
  addr0 : forall x, add x zero = x; (*        wrt add. *)
}.

HB.structure Definition Monoid := { M of is_monoid M }.

HB.instance Definition Z_is_monoid : is_monoid Z :=
  is_monoid.Build Z 0%Z Z.add Z.add_assoc Z.add_0_l Z.add_0_r.