~/jendhub

def internal_sorted_cons_test

bend-mathlib@0.8.1.0 · list.bend:835

import bend-mathlib@0.8.1.0/list.bend as List
import Base

835# The cons step of sorted_by's pairs with the head written as (x, y): internal_all_cons_test at a variable pair head is outside what --verdict can check.
836def internal_sorted_cons_test(~A: Data, ~le: A -> A -> Bool, -x: A, -y: A, -z: List<&1, A & A>, b: Bool, e: {le(x, y) == b : Bool}) -> {Bool.and(b, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z)) == List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), (x, y) <> z) : Bool}:
837  %Equal.sym(Bool, le(x, y), b, e) : {Bool.and(b, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z)) == List.all.if(u => List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z), _) : Bool}
838  internal_all_if(b, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z))

Uses (11)

Used by (2)