Blockchain.v 488 Bytes
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
From Coq Require Import String.
2
From Coq Require OrderedTypeEx.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
3

4
5
6
7
8
Definition address := nat.
Definition amount := nat.
Definition block_id := nat.
Definition block_hash := string.
Definition version := nat.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
9

10
11
Inductive tx_body :=
| Empty : tx_body.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
12

13
14
15
16
Record contract_call_details :=
  { from : address ;
    to : address ;
    value : amount
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
17
18
  }.

19
20
21
22
23
Module Address.
  Definition eqb := Nat.eqb.
  Module as_modern_OT := PeanoNat.Nat.
  Module as_old_OT := OrderedTypeEx.Nat_as_OT.
End Address.