package octez-proto-libs

  1. Overview
  2. Docs
Octez protocol libraries

Install 

dune-project
 Dependency

www.tezos.com Readme Edit opam file Versions (5)

Authors

  1. T
    Tezos devteam

Maintainers

  1. C
    contact@tezos.com

Sources

tezos-octez-v20.1.tag.bz2
sha256=ddfb5076eeb0b32ac21c1eed44e8fc86a6743ef18ab23fff02d36e365bb73d61
sha512=d22a827df5146e0aa274df48bc2150b098177ff7e5eab52c6109e867eb0a1f0ec63e6bfbb0e3645a6c2112de3877c91a17df32ccbff301891ce4ba630c997a65

doc/octez-proto-libs.protocol-environment/Tezos_protocol_environment/V8/Make/Equality_witness/index.html

Module Make.Equality_witnessSource

This module provides support for type equalities and runtime type identifiers.

For two types a and b, (a, b) eq is a witness that a = b. This is a standard generalized algebraic datatype on top of which type-level programming techniques can be implemented.

Given a type a, an inhabitant of a t is a dynamic identifier for a. Identifiers can be compared for equality. They are also equipped with a hash function.

WARNING: the hash function changes at every run. Therefore, the result of the hash function should never be stored.

Notice that dynamic identifiers are not unique: two identifiers for a can have distinct hash and can be physically distinct. Hence, only eq can decide if two type identifiers correspond to the same type.

Sourcetype (_, _) eq =
  1. | Refl : ('a, 'a) eq

A proof witness that two types are equal.

Sourcetype 'a t

A dynamic representation for 'a.

Sourceval make : unit -> 'a t

make () is a dynamic representation for 'a. A fresh identifier is returned each time make () is evaluated.

Sourceval eq : 'a t -> 'b t -> ('a, 'b) eq option

eq ida idb returns a proof that a = b if ida and idb identify the same type.

Sourceval hash : 'a t -> int

hash id returns a hash for id.