proofs/lib/lemmas/src/time.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/time.bend as Time

3 imports

import Base
import ../types/model.bend as T
import ./wide.bend as W

Definitions

def add source · line 5 · raw

@a:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> @b:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64

def milliseconds source · line 10 · raw

@ns:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64

def is_zero source · line 14 · raw

@t:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> Bool

def deadline_choose source · line 18 · raw

@now:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> @ns:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> @immortal:Bool -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64

def deadline source · line 25 · raw

@now:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> @+ns:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64

def le source · line 28 · raw

@a:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> @b:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> Bool

def expired_choose source · line 33 · raw

@d:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> @now:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> @immortal:Bool -> Bool

def expired source · line 40 · raw

@+deadline:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> @now:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.Int64 -> Bool