Commit 0434f918 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Add beq_address

parent 468d8467
Pipeline #10611 passed with stage
in 2 minutes and 1 second
Require Import Coq.Strings.String.
Require Import List.
Import ListNotations.
From Coq Require Import String.
Definition Address := nat.
Definition Amount := nat.
......@@ -26,4 +24,6 @@ Record StoredContract :=
{
stateTy : Type ;
contract : Contract stateTy
}.
\ No newline at end of file
}.
Definition beq_address := Nat.eqb.
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment