package tezos-protocol-017-PtNairob

  1. Overview
  2. Docs
package tezos-protocol-017-PtNairob
Legend:
Library
Module
Module type
Parameter
Class
Class type

Dependent booleans

type no = private
  1. | DNo
type yes = private
  1. | DYes
type _ dbool =
  1. | No : no dbool
  2. | Yes : yes dbool

'b dbool is a boolean whose value depends on its type parameter 'b. yes dbool can only be Yes. no dbool can only be No.

type ('a, 'b, 'r) dand =
  1. | NoNo : (no, no, no) dand
  2. | NoYes : (no, yes, no) dand
  3. | YesNo : (yes, no, no) dand
  4. | YesYes : (yes, yes, yes) dand

('a, 'b, 'r) dand is a witness of the logical conjunction of dependent booleans. 'r is the result of 'a and 'b.

type ('a, 'b) ex_dand =
  1. | Ex_dand : ('a, 'b, _) dand -> ('a, 'b) ex_dand
val dand : 'a dbool -> 'b dbool -> ('a, 'b) ex_dand

Logical conjunction of dependent booleans.

val dbool_of_dand : ('a, 'b, 'r) dand -> 'r dbool

Result of the logical conjunction of dependent booleans.

type (_, _) eq =
  1. | Eq : ('a, 'a) eq

Type equality witness.

val merge_dand : ('a, 'b, 'c1) dand -> ('a, 'b, 'c2) dand -> ('c1, 'c2) eq

merge_dand proves that the type dand represents a function, i.e. that there is a unique 'r such that ('a, 'b, 'r) dand is inhabited for a given 'a and a given 'b.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct