Skip to main content

🗳️ Voting_period_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Voting_period_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Voting_period_repr.

[get_current] after [init] is valid, as long as the value used in the initialization is valid