~/bend-docscommunity

proofs/lib/logic.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as Logic

1 import
import Base

Definitions

def truth source · line 5 · raw

@b:Bool -> Type

def false_true source · line 12 · raw

@e:{False{} == True{} : Bool} -> Empty

def true_false source · line 16 · raw

@e:{True{} == False{} : Bool} -> Empty

def and_left source · line 19 · raw

@a:Bool -> @b:Bool -> @e:{Bool.and(a, b) == True{} : Bool} -> {a == True{} : Bool}

def and_right source · line 26 · raw

@a:Bool -> @b:Bool -> @e:{Bool.and(a, b) == True{} : Bool} -> {b == True{} : Bool}

def and_intro source · line 33 · raw

@a:Bool -> @b:Bool -> @ea:{a == True{} : Bool} -> @eb:{b == True{} : Bool} -> {Bool.and(a, b) == True{} : Bool}

def not_true source · line 37 · raw

@b:Bool -> @e:{Bool.not(b) == True{} : Bool} -> {b == False{} : Bool}

def not_false source · line 44 · raw

@b:Bool -> @e:{b == False{} : Bool} -> {Bool.not(b) == True{} : Bool}

def bool_cases source · line 48 · raw

@b:Bool -> Or({b == True{} : Bool}, {b == False{} : Bool})

def true_not_false source · line 55 · raw

@b:Bool -> @t:{b == True{} : Bool} -> @f:{b == False{} : Bool} -> Empty

def cmp_code source · line 59 · raw

@c:Cmp -> Nat

Cmp discrimination.

def cmp_lt_eq source · line 68 · raw

@e:{LT{} == EQ{} : Cmp} -> Empty

def cmp_lt_gt source · line 72 · raw

@e:{LT{} == GT{} : Cmp} -> Empty

def cmp_eq_gt source · line 76 · raw

@e:{EQ{} == GT{} : Cmp} -> Empty

def none_some source · line 81 · raw

@-A:Data -> @x:A -> @e:{None{} == Some{x} : Maybe<&2, A>} -> Empty

Maybe discrimination.

def some_value source · line 85 · raw

@-A:Data -> @m:Maybe<&2, A> -> @d:A -> A

def some_inj source · line 92 · raw

@-A:Data -> @x:A -> @y:A -> @e:{Some{x} == Some{y} : Maybe<&2, A>} -> {x == y : A}

def pair_fst source · line 95 · raw

@-A:Type -> @-B:Type -> @a:A -> @b:B -> @c:A -> @d:B -> @e:{(a, b) == (c, d) : Pair(A, B)} -> {a == c : A}

def pair_snd source · line 98 · raw

@-A:Type -> @-B:Type -> @a:A -> @b:B -> @c:A -> @d:B -> @e:{(a, b) == (c, d) : Pair(A, B)} -> {b == d : B}

def pair_eq source · line 101 · raw

@-A:Type -> @-B:Type -> @a:A -> @b:B -> @c:A -> @d:B -> @ea:{a == c : A} -> @eb:{b == d : B} -> {(a, b) == (c, d) : Pair(A, B)}

def subst source · line 107 · raw

@-A:Type -> @-P:(@_:A -> Type) -> @-a:A -> @-b:A -> @e:{a == b : A} -> @pa:P(a) -> P(b)

Transport a proof along an equation.

def sfst source · line 112 · raw

@-A:Type -> @-B:(@-x:A -> Type) -> @p:Sigma<&1, &1, A, B> -> A

Dependent pair projections (call results cannot be destructured directly).

def ssnd source · line 117 · raw

@-A:Type -> @-B:(@-x:A -> Type) -> @p:Sigma<&1, &1, A, B> -> B(sfst(A, B, p))

def pair_eta source · line 122 · raw

@-A:Type -> @-B:Type -> @p:Pair(A, B) -> {p == (Pair.fst(A, B, p), Pair.snd(A, B, p)) : Pair(A, B)}