blob: 1f57ce84713bbc7cba610cd5752f7173ebad3d09 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Require Import Ring_base.
Record word : Type := Build_word
{ rep : Type;
zero : rep; one: rep;
add : rep -> rep -> rep;
sub : rep -> rep -> rep;
opp : rep -> rep;
mul : rep -> rep -> rep;
}.
Axiom rth
: forall (word : word ),
@ring_theory (@rep word)
(@zero word)
(@one word) (@add word)
(@mul word) (@sub word)
(@opp word) (@eq (@rep word)).
Fail Add Ring wring: (@rth _).
|
