blob: 8d4e73dfac05dacb6e64174b3de4acf63132fb61 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Module Type Sig.
Parameter add: nat -> nat -> nat.
Axiom homework: forall (a b: nat), add a b = add b a.
End Sig.
Module Impl.
Definition add(a b: nat) := plus a b.
Axiom homework: forall (a b: nat), add 0 b = add b 0.
End Impl.
Module M : Sig := Impl.
|
