std

Nat

data Nat

The unary natural numbers: zero and successor.

Nat.add

def Nat.add (m : Nat) (n : Nat) : Nat

Natural-number addition, by recursion on the first argument.

Nat.mul

def Nat.mul (m : Nat) (n : Nat) : Nat

Natural-number multiplication, as repeated addition on the first argument.

Nat.sub

def Nat.sub (m : Nat) (n : Nat) : Nat

Truncated natural-number subtraction: m - n, or zero when n exceeds m.

Bool

data Bool

The booleans true and false.

Bool.and

def Bool.and (a : Bool) (b : Bool) : Bool

Boolean conjunction.

Bool.leftOfAnd

def Bool.leftOfAnd (a : Bool) (b : Bool) : and a b = true -> a = true

The left side of a true conjunction is true.

Bool.rightOfAnd

def Bool.rightOfAnd (a : Bool) (b : Bool) : and a b = true -> b = true

The right side of a true conjunction is true.

Bool.andOfBoth

def Bool.andOfBoth (a : Bool) (b : Bool) : a = true -> b = true -> and a b = true

Both sides of a conjunction true make it true.

Bool.or

def Bool.or (a : Bool) (b : Bool) : Bool

Boolean disjunction.

Bool.not

def Bool.not (a : Bool) : Bool

Boolean negation.

Bool.dite

def Bool.dite {l : Level} {A : Type l} (c : Bool) (t : c = true -> A) (e : c = false -> A) : A

If-then-else whose branches receive the proof of the condition (what termination_by turns an if into).

Nat.beq

def Nat.beq (m : Nat) (n : Nat) : Bool

Boolean equality test on natural numbers.

Nat.blt

def Nat.blt (m : Nat) (n : Nat) : Bool

Boolean strict less-than test on natural numbers: m < n.

Nat.ble

def Nat.ble (m : Nat) (n : Nat) : Bool

Boolean less-than-or-equal test on natural numbers: m <= n.

Nat.bleOfBlt

def Nat.bleOfBlt (m : Nat) (n : Nat) (h : Nat.blt m n = true) : Nat.ble m n = true

Strictly less implies less or equal: m < n gives m <= n.

Nat.bgt

def Nat.bgt (m : Nat) (n : Nat) : Bool

Boolean strict greater-than test on natural numbers: m > n.

Nat.divAuxFuel

def Nat.divAuxFuel (fuel : Nat) (q : Nat) (m : Nat) (n : Nat) : Nat

Division by repeated subtraction with an accumulator q, bounded by fuel; stops when m < n, when n is zero, or when fuel runs out.

Nat.modAuxFuel

def Nat.modAuxFuel (fuel : Nat) (m : Nat) (n : Nat) : Nat

Remainder by repeated subtraction, bounded by fuel; returns m unchanged when n is zero.

Nat.div

def Nat.div (m : Nat) (n : Nat) : Nat

Natural-number division m / n, rounding down; division by zero gives zero.

Nat.mod

def Nat.mod (m : Nat) (n : Nat) : Nat

Natural-number remainder m mod n; the remainder modulo zero is m itself.

Nat.bge

def Nat.bge (m : Nat) (n : Nat) : Bool

Boolean greater-than-or-equal test on natural numbers: m ≥ n.

Nat.bitwiseAndFuel

def Nat.bitwiseAndFuel (fuel : Nat) (m : Nat) (n : Nat) : Nat

Bitwise and of the lowest fuel bits of m and n.

Nat.bitwiseOrFuel

def Nat.bitwiseOrFuel (fuel : Nat) (m : Nat) (n : Nat) : Nat

Bitwise or of the lowest fuel bits of m and n.

Nat.bitwiseXorFuel

def Nat.bitwiseXorFuel (fuel : Nat) (m : Nat) (n : Nat) : Nat

Bitwise exclusive or of the lowest fuel bits of m and n.

Nat.bitwiseAnd

def Nat.bitwiseAnd (m : Nat) (n : Nat) : Nat

Bitwise and of natural numbers.

Nat.bitwiseOr

def Nat.bitwiseOr (m : Nat) (n : Nat) : Nat

Bitwise or of natural numbers.

Nat.bitwiseXor

def Nat.bitwiseXor (m : Nat) (n : Nat) : Nat

Bitwise exclusive or of natural numbers.

Nat.min

def Nat.min (m : Nat) (n : Nat) : Nat

The smaller of two natural numbers.

Nat.max

def Nat.max (m : Nat) (n : Nat) : Nat

The larger of two natural numbers.

Nat.maxSucc

def Nat.maxSucc (j : Nat) (k : Nat) : succ (max j k) = max (succ j) (succ k)

Successor distributes over max: succ (max j k) = max (succ j) (succ k).

Nat.maxComm

def Nat.maxComm (m : Nat) (n : Nat) : max m n = max n m

Commutativity of max on natural numbers: max m n = max n m.

Option

data Option (A : Type)

An optional value: nothing, or just a value of type A.

Option.withDefault

def Option.withDefault {A : Type} (default : A) (mx : Option A) : A

The value inside a Maybe, or the given default when it is nothing.

Option.isSome

def Option.isSome {A : Type} (mx : Option A) : Bool

Boolean test for whether a Maybe holds a value.

Option.isNone

def Option.isNone {A : Type} (mx : Option A) : Bool

Boolean test for whether a Maybe is nothing.

Option.map

def Option.map {A B : Type} (f : A -> B) (mx : Option A) : Option B

Apply a function to the value inside a Maybe, if any.

Pair

data Pair (A : Type) (B : Type)

A pair of a value of type A and a value of type B.

keepType

def keepType {A : Type} (old : A) (new : A) : A

Return the new value, constrained to have the same type as the old one; used to desugar assignment to a let mut variable.

Pair.fstPair

def Pair.fstPair {A B : Type} (p : Pair A B) : A

The first component of a Pair.

Pair.sndPair

def Pair.sndPair {A B : Type} (p : Pair A B) : B

The second component of a Pair.

Either

data Either (A : Type) (B : Type)

A value that is either a left A or a right B.

Either.bimap

def Either.bimap {A B C D : Type} (f : A -> C) (g : B -> D) (e : Either A B) : Either C D

One function applied to a left value, another to a right value.

Either.mapLeft

def Either.mapLeft {A B C : Type} (f : A -> C) (e : Either A B) : Either C B

A function applied to a left value; a right value stays.

Either.mapRight

def Either.mapRight {A B D : Type} (g : B -> D) (e : Either A B) : Either A D

A function applied to a right value; a left value stays.

Either.swapSides

def Either.swapSides {A B : Type} (e : Either A B) : Either B A

The sides swapped: a left becomes a right and the other way round.

Either.isLeft

def Either.isLeft {A B : Type} (e : Either A B) : Bool

Whether it is a left value.

Either.isRight

def Either.isRight {A B : Type} (e : Either A B) : Bool

Whether it is a right value.

Either.fromLeft

def Either.fromLeft {A B : Type} (default : A) (e : Either A B) : A

The value inside a left, or default for a right.

Either.fromRight

def Either.fromRight {A B : Type} (default : B) (e : Either A B) : B

The value inside a right, or default for a left.

Either.fold

def Either.fold {A B C : Type} (f : A -> C) (g : B -> C) (e : Either A B) : C

f of a left value, g of a right value.

List

data List (A : Type)

Finite lists: nil, or an element consed onto a list.

List.map

def List.map {A B : Type} (f : A -> B) (xs : List A) : List B

Apply a function to every element of a list.

List.filter

def List.filter {A : Type} (p : A -> Bool) (xs : List A) : List A

Keep the elements of a list that satisfy a boolean predicate.

List.append

def List.append {A : Type} (xs : List A) (ys : List A) : List A

Concatenate two lists.

List.length

def List.length {A : Type} (xs : List A) : Nat

The number of elements in a list.

List.listHead

def List.listHead {A : Type} (default : A) (xs : List A) : A

The first element of a list, or the given default for an empty list.

List.listTail

def List.listTail {A : Type} (xs : List A) : List A

A list without its first element; the empty list stays empty.

List.revAcc

def List.revAcc {A : Type} (xs : List A) (acc : List A) : List A

Reverse xs onto the front of the accumulator acc; the helper behind reverse.

List.reverse

def List.reverse {A : Type} (xs : List A) : List A

Reverse a list.

List.foldl

def List.foldl {A B : Type} (f : B -> A -> B) (z : B) (xs : List A) : B

Left fold: combine the elements from left to right, starting from z.

List.foldr

def List.foldr {A B : Type} (f : A -> B -> B) (z : B) (xs : List A) : B

Right fold: combine the elements from right to left, ending with z.

List.take

def List.take {A : Type} (n : Nat) (xs : List A) : List A

The first n elements of a list (or the whole list if it is shorter).

List.drop

def List.drop {A : Type} (n : Nat) (xs : List A) : List A

A list without its first n elements.

List.replicate

def List.replicate {A : Type} (n : Nat) (x : A) : List A

A list of n copies of x.

List.rangeAcc

def List.rangeAcc (n : Nat) (acc : List Nat) : List Nat

The numbers 0 to n - 1 prepended to acc; the helper behind range.

List.range

def List.range (n : Nat) : List Nat

The list of natural numbers 0, 1, …, n - 1.

Nat.addZeroR

def Nat.addZeroR (m : Nat) : add m zero = m

Zero is a right identity for addition: m + 0 = m.

Nat.addSuccR

def Nat.addSuccR (m : Nat) (n : Nat) : add m (succ n) = succ (add m n)

Successor in the right summand moves outside: m + succ n = succ (m + n).

Nat.addAssoc

def Nat.addAssoc (m : Nat) (n : Nat) (o : Nat) : add m (add n o) = add (add m n) o

Associativity of natural-number addition, right-nested to left-nested: m + (n + o) = (m + n) + o.

Bool.notnot

def Bool.notnot (x : Bool) : not (not x) = x

Boolean negation is an involution: not (not x) = x.

Bool.andTrue

def Bool.andTrue (a : Bool) : and a true = a

True is a right identity for conjunction: and a true = a.

Bool.orFalse

def Bool.orFalse (a : Bool) : or a false = a

False is a right identity for disjunction: or a false = a.

Bool.andFalse

def Bool.andFalse (a : Bool) : and a false = false

False absorbs conjunction on the right: and a false = false.

Bool.orTrue

def Bool.orTrue (a : Bool) : or a true = true

True absorbs disjunction on the right: or a true = true.

Bool.notTrue

def Bool.notTrue : not true = false

The negation of true is false.

Bool.notFalse

def Bool.notFalse : not false = true

The negation of false is true.

Nat.addZeroL

def Nat.addZeroL (m : Nat) : add zero m = m

Zero is a left identity for addition: 0 + m = m.

Nat.addComm

def Nat.addComm (m : Nat) (n : Nat) : add m n = add n m

Commutativity of natural-number addition: m + n = n + m.

List.appendNil

def List.appendNil {A : Type} (xs : List A) : append xs nil = xs

The empty list is a right identity for append: append xs nil = xs.

Nat.subZero

def Nat.subZero (m : Nat) : sub m zero = m

Zero is a right identity for truncated subtraction: m - 0 = m.

Nat.mulZeroR

def Nat.mulZeroR (m : Nat) : mul m zero = zero

Zero absorbs multiplication on the right: m * 0 = 0.

Nat.mulOneR

def Nat.mulOneR (m : Nat) : mul m (succ zero) = m

One is a right identity for multiplication: m * 1 = m.

Nat.addSwap

def Nat.addSwap (n : Nat) (k : Nat) (x : Nat) : add n (add k x) = add k (add n x)

Swap the first two summands of a right-nested sum: n + (k + x) = k + (n + x).

Nat.mulSuccR

def Nat.mulSuccR (m : Nat) (n : Nat) : mul m (succ n) = add m (mul m n)

Multiplication by a successor adds one copy: m * succ n = m + m * n.

List.nthOption

def List.nthOption {A : Type} (xs : List A) (n : Nat) : Option A

Returns the element at the given index, or none when the index is out of range.

List.headOption

def List.headOption {A : Type} (xs : List A) : Option A

The first element of a list, or none for an empty list.

List.zip

def List.zip {A B : Type} (xs : List A) (ys : List B) : List (Pair A B)

Pair up corresponding elements of two lists, stopping at the shorter one.

List.zip3

def List.zip3 {A B C : Type} (xs : List A) (ys : List B) (zs : List C) : List (Pair A (Pair B C))

Combine three lists elementwise into right-nested triples, stopping at the shortest.

List.enumerate

def List.enumerate {A : Type} (xs : List A) : List (Pair Nat A)

Pair every element of a list with its index, counting from 0.

concat

def concat {A : Type} (xss : List (List A)) : List A

Flatten a list of lists into one list.

List.concatMap

def List.concatMap {A B : Type} (f : A -> List B) (xs : List A) : List B

Map each element to a list and concatenate the results.

Monad

class Monad (M : Type -> Type)

A monad: pure puts a value in, bind runs a computation and feeds its result to the next one. do blocks are written with these.

monadOption

instance monadOption : Monad Option

Maybe is a monad: bind stops at the first nothing.

monadEither

instance monadEither (E : Type) : Monad (Either E)

Either E is a monad: bind stops at the first left.

monadList

instance monadList : Monad List

List is a monad: bind maps each element to a list and concatenates the results.

LoopCtl

data LoopCtl (S : Type)

Loop body result for loops using break or continue: continue with a state, or stop with a state.

LoopStep

data LoopStep (R : Type) (S : Type)

Loop body result for loops using return: continue, break, or return a value early.

forInListM

def forInListM {M : Type -> Type} {{inst : Monad M}} {A : Type} {S : Type} (xs : List A) (s : S) (f : A -> S -> M S) : M S

Expansion of for x in xs do ... in any monad: runs f on each element in order, threading a state through.

forInListCtlM

def forInListCtlM {M : Type -> Type} {{inst : Monad M}} {A : Type} {S : Type} (xs : List A) (s : S) (f : A -> S -> M (LoopCtl S)) : M S

Like forInListM, for loops using break or continue.

forInListRM

def forInListRM {M : Type -> Type} {{inst : Monad M}} {A : Type} {R : Type} {S : Type} (xs : List A) (s : S) (f : A -> S -> M (LoopStep R S)) : M (Either R S)

Like forInListM, for loops using return: left v is an early return, right s the state at the end.

List.any

def List.any {A : Type} (p : A -> Bool) (xs : List A) : Bool

Whether some element of the list satisfies the predicate.

List.all

def List.all {A : Type} (p : A -> Bool) (xs : List A) : Bool

Whether every element of the list satisfies the predicate.

List.elemNat

def List.elemNat (x : Nat) (xs : List Nat) : Bool

Whether a natural number occurs in a list of natural numbers.

List.mapAppend

def List.mapAppend {A B : Type} (f : A -> B) (xs : List A) (ys : List A) : map f (append xs ys) = append (map f xs) (map f ys)

Mapping over an append is appending the maps: map f (xs ++ ys) = map f xs ++ map f ys.

List.lengthAppend

def List.lengthAppend {A : Type} (xs : List A) (ys : List A) : length (append xs ys) = add (length xs) (length ys)

The length of an append is the sum of the lengths: length (xs ++ ys) = length xs + length ys.

Unit

data Unit

The unit type, with the single element unit.

isContrUnit

def isContrUnit : (center : Unit) × ((x : Unit) -> center ≡ x)

The unit type is contractible.

Empty

data Empty

The empty type, with no constructors.

Dec

data Dec (A : Type)

A decision for A: either an element of A or a refutation of A.

absurd

def absurd {A : Type} (e : Empty) : A

Ex falso: from an element of Empty, produce an element of any type.

Nat.pred

def Nat.pred (n : Nat) : Nat

Predecessor of a natural number, sending zero to zero.

Nat.addSuccL

def Nat.addSuccL (m : Nat) (n : Nat) : add (succ m) n = succ (add m n)

Successor in the left summand moves outside: succ m + n = succ (m + n).

Nat.double

def Nat.double (n : Nat) : Nat

Double a natural number: n + n.

Bool.andComm

def Bool.andComm (a : Bool) (b : Bool) : and a b = and b a

Commutativity of boolean conjunction: and a b = and b a.

Bool.orComm

def Bool.orComm (a : Bool) (b : Bool) : or a b = or b a

Commutativity of boolean disjunction: or a b = or b a.

Bool.andAssoc

def Bool.andAssoc (a : Bool) (b : Bool) (c : Bool) : and (and a b) c = and a (and b c)

Associativity of boolean conjunction: and (and a b) c = and a (and b c).

Bool.orAssoc

def Bool.orAssoc (a : Bool) (b : Bool) (c : Bool) : or (or a b) c = or a (or b c)

Associativity of boolean disjunction: or (or a b) c = or a (or b c).

Bool.deMorgan1

def Bool.deMorgan1 (a : Bool) (b : Bool) : not (and a b) = or (not a) (not b)

De Morgan’s law for conjunction: not (and a b) = or (not a) (not b).

Bool.deMorgan2

def Bool.deMorgan2 (a : Bool) (b : Bool) : not (or a b) = and (not a) (not b)

De Morgan’s law for disjunction: not (or a b) = and (not a) (not b).

Nat.isZero

def Nat.isZero (n : Nat) : Bool

Boolean test for whether a natural number is zero.

Nat.isSucc

def Nat.isSucc (n : Nat) : Bool

Boolean test for whether a natural number is a successor (nonzero).

Nat.pow

def Nat.pow (m : Nat) (n : Nat) : Nat

Natural-number exponentiation: m ^ n.

Nat.factorial

def Nat.factorial (n : Nat) : Nat

Factorial: n! = n * (n - 1) * … * 1, with 0! = 1.

Nat.fibAcc

def Nat.fibAcc (n : Nat) (a : Nat) (b : Nat) : Nat

Fibonacci helper: run n steps of (a, b) to (b, a + b) and return a.

Nat.fib

def Nat.fib (n : Nat) : Nat

The n-th Fibonacci number, with fib 0 = 0 and fib 1 = 1.

id

def id {A : Type} (a : A) : A

The identity function.

const

def const {A B : Type} (a : A) (b : B) : A

The constant function: return a and ignore b.

List.appendAssoc

def List.appendAssoc {A : Type} (xs : List A) (ys : List A) (zs : List A) : append (append xs ys) zs = append xs (append ys zs)

Associativity of list append: (xs ++ ys) ++ zs = xs ++ (ys ++ zs).

List.mapId

def List.mapId {A : Type} (xs : List A) : map (fun (x : A) => x) xs = xs

Mapping the identity function over a list changes nothing.

List.lengthMap

def List.lengthMap {A B : Type} (f : A -> B) (xs : List A) : length (map f xs) = length xs

Mapping preserves length: length (map f xs) = length xs.

List.lengthReplicate

def List.lengthReplicate {A : Type} (n : Nat) (x : A) : length (replicate n x) = n

A list of n copies has length n.

Le

data Le : Nat -> Nat -> Type

The inductive <= relation on naturals: Le m n holds when m <= n (0 <= n, and m <= n gives m + 1 <= n + 1).

Nat.addOneSucc

def Nat.addOneSucc (m : Nat) : add m (succ zero) = succ m

Adding one is the successor: m + 1 = succ m.

List.intersperse

def List.intersperse {A : Type} (sep : A) (xs : List A) : List A

Put the separator between every two adjacent elements of a list.

List.partition

def List.partition {A : Type} (p : A -> Bool) (xs : List A) : Pair (List A) (List A)

Split a list into the elements that satisfy a predicate and those that do not, keeping order.

List.span

def List.span {A : Type} (p : A -> Bool) (xs : List A) : Pair (List A) (List A)

Split a list at the first element failing the predicate: the longest satisfying prefix and the rest.

List.takeWhile

def List.takeWhile {A : Type} (p : A -> Bool) (xs : List A) : List A

The longest prefix of a list whose elements satisfy the predicate.

List.dropWhile

def List.dropWhile {A : Type} (p : A -> Bool) (xs : List A) : List A

A list without its longest prefix of elements satisfying the predicate.

List.find

def List.find {A : Type} (p : A -> Bool) (xs : List A) : Option A

The first element of a list that satisfies the predicate, or nothing.

Nat.iterate

def Nat.iterate {A : Type} (n : Nat) (f : A -> A) (x : A) : A

Apply f to x n times.

List.sum

def List.sum (xs : List Nat) : Nat

The sum of a list of natural numbers.

List.product

def List.product (xs : List Nat) : Nat

The product of a list of natural numbers.

Nat.mulZeroL

def Nat.mulZeroL (n : Nat) : mul zero n = zero

Zero absorbs multiplication on the left: 0 * n = 0.

Nat.mulOneL

def Nat.mulOneL (n : Nat) : mul (succ zero) n = n

One is a left identity for multiplication: 1 * n = n.

Nat.beqRefl

def Nat.beqRefl (n : Nat) : Nat.beq n n = true

Boolean equality on natural numbers is reflexive: Nat.beq n n = true.

Option.bind

def Option.bind {A B : Type} (mx : Option A) (f : A -> Option B) : Option B

Monadic bind for Maybe: apply f to the value if there is one, otherwise nothing.

Option.orElse

def Option.orElse {A : Type} (mx : Option A) (my : Option A) : Option A

The first Maybe if it holds a value, otherwise the second.

catMaybes

def catMaybes {A : Type} (xs : List (Option A)) : List A

Keep the values of the just elements of a list, dropping the nothings.

List.mapOptionFn

def List.mapOptionFn {A B : Type} (f : A -> Option B) (xs : List A) : List B

Apply a partial function to every element, keeping only the successful results.

apply

def apply {A B : Type} (f : A -> B) (x : A) : B

Function application: apply f x = f x.

Stream

codata Stream {i : Size} (A : Type)

Infinite streams, as a sized coinductive type with head and tail.

Stream.zeros

def Stream.zeros : Stream Nat

The stream of all zeros.

Stream.nats_from

def Stream.nats_from (n : Nat) : Stream Nat

The stream n, n + 1, n + 2, …

Stream.nats

def Stream.nats : Stream Nat

The stream of all natural numbers 0, 1, 2, …

Stream.repeat

def Stream.repeat {A : Type} (a : A) : Stream A

The stream that repeats a forever.

CoNat

codata CoNat {i : Size}

Conatural numbers (possibly infinite), observed through an optional predecessor.

CoNat.coZero

def CoNat.coZero : CoNat

The conatural zero, which has no predecessor.

CoNat.coSucc

def CoNat.coSucc (n : CoNat) : CoNat

The conatural successor of n.

CoNat.infinity

def CoNat.infinity : CoNat

The infinite conatural number, its own predecessor.

Stream.take_stream

def Stream.take_stream {A : Type} (n : Nat) (s : Stream A) : List A

The first n elements of a stream, as a list.

Stream.map_stream

def Stream.map_stream {A B : Type} (f : A -> B) (s : Stream A) : Stream B

Apply a function to every element of a stream.

Stream.iterate_stream

def Stream.iterate_stream {A : Type} (f : A -> A) (a : A) : Stream A

The stream a, f a, f (f a), …

Stream.zipWith_stream

def Stream.zipWith_stream {A B : Type} {C : Type} (f : A -> B -> C) (s1 : Stream A) (s2 : Stream B) : Stream C

Combine two streams elementwise with a function.

Stream.drop_stream

def Stream.drop_stream {A : Type} (n : Nat) (s : Stream A) : Stream A

A stream without its first n elements.

Stream.interleave

def Stream.interleave {A : Type} (s1 : Stream A) (s2 : Stream A) : Stream A

Alternate the elements of two streams, starting with the first.

CoNat.fromNat

def CoNat.fromNat (n : Nat) : CoNat

Embed a natural number into the conatural numbers.

Colist

codata Colist {i : Size} (A : Type)

Possibly infinite lists, observed through uncons: nothing for empty, or a head and a tail.

conil

def conil (A : Type) : Colist A

The empty colist.

cocons

def cocons (A : Type) (x : A) (xs : Colist A) : Colist A

Prepend an element to a colist.

fromList

def fromList (A : Type) (xs : List A) : Colist A

Convert a finite list into a colist.

CoTree

codata CoTree {i : Size} (A : Type)

Infinite binary trees with a label and left and right subtrees.

const_tree

def const_tree (A : Type) (a : A) : CoTree A

The infinite binary tree whose every label is a.

Process

codata Process {i : Size} (I : Type) (O : Type)

A pure coinductive process that, on each input, produces an output and the next process.

Process.echoProcess

def Process.echoProcess : Process Nat Nat

The process that outputs each natural-number input unchanged, forever.

M

codata M {i : Size} (S : Type) (P : S -> Type)

The general coinductive M-type: a shape together with subtrees indexed by the positions of that shape.

Bool.xor

def Bool.xor (a : Bool) (b : Bool) : Bool

Boolean exclusive or.

Bool.xorComm

def Bool.xorComm (a : Bool) (b : Bool) : xor a b = xor b a

Commutativity of exclusive or: xor a b = xor b a.

Bool.xorFalse

def Bool.xorFalse (a : Bool) : xor a false = a

False is a right identity for exclusive or: xor a false = a.

Bool.xorSelf

def Bool.xorSelf (a : Bool) : xor a a = false

Anything exclusive-or itself is false: xor a a = false.

Bool.implies

def Bool.implies (a : Bool) (b : Bool) : Bool

Boolean implication: not a or b.

List.filterTrue

def List.filterTrue {A : Type} (xs : List A) : filter (fun (x : A) => true) xs = xs

Filtering with the always-true predicate keeps the whole list.

List.filterFalse

def List.filterFalse {A : Type} (xs : List A) : filter (fun (x : A) => false) xs = nil

Filtering with the always-false predicate gives the empty list.

Pair.swapPair

def Pair.swapPair {A B : Type} (p : Pair A B) : Pair B A

Swap the two components of a Pair.

Pair.mapPair

def Pair.mapPair {A B : Type} {C : Type} {D : Type} (f : A -> C) (g : B -> D) (p : Pair A B) : Pair C D

Apply one function to each component of a Pair.

List.nth

def List.nth {A : Type} (default : A) (n : Nat) (xs : List A) : A

The element at index n of a list (counting from 0), or the default when the index is out of range.

List.snoc

def List.snoc {A : Type} (xs : List A) (x : A) : List A

Append an element at the end of a list.

List.last

def List.last {A : Type} (default : A) (xs : List A) : A

The last element of a list, or the default for an empty list.

List.initList

def List.initList {A : Type} (xs : List A) : List A

A list without its last element; the empty list stays empty.

List.mapNil

def List.mapNil {A B : Type} (f : A -> B) : map f (nil : List A) = (nil : List B)

Mapping over the empty list gives the empty list.

List.mapSingleton

def List.mapSingleton {A B : Type} (f : A -> B) (x : A) : map f (cons x nil) = cons (f x) (nil : List B)

Mapping over a one-element list: map f [x] = [f x].

List.lengthSingleton

def List.lengthSingleton {A : Type} (x : A) : length (cons x (nil : List A)) = succ zero

A one-element list has length one.

List.reverseNilStd

def List.reverseNilStd {A : Type} : reverse (nil : List A) = (nil : List A)

Reversing the empty list gives the empty list.

List.foldlNil

def List.foldlNil {A B : Type} (f : B -> A -> B) (z : B) : foldl f z (nil : List A) = z

A left fold over the empty list returns the initial value.

List.foldrNil

def List.foldrNil {A B : Type} (f : A -> B -> B) (z : B) : foldr f z (nil : List A) = z

A right fold over the empty list returns the initial value.

Pair.swapPairInvol

def Pair.swapPairInvol {A B : Type} (p : Pair A B) : swapPair (swapPair p) = p

Swapping a Pair twice gives it back.

Pair.mapPairId

def Pair.mapPairId {A B : Type} (p : Pair A B) : mapPair (fun (a : A) => a) (fun (b : B) => b) p = p

Mapping identity functions over both components of a Pair changes nothing.

Pos

data Pos

Positive binary numbers, least significant bit outermost: xH is 1, xO p is 2p, xI p is 2p + 1.

Bin

data Bin

Binary natural numbers: zero, or a positive binary number.

Char

data Char

A character, given by its Unicode code point in binary.

String

data String

A string, as a list of characters.

OptionPrim

data OptionPrim (A : Type)

A local optional type used as the result of construct, to signal that reconstruction failed.

Principal

data Principal

An owner identity, named by a string; used by the ownership predicate Owns.

proofIrrelevantTag

def proofIrrelevantTag (0 _tag : Nat) (n : Nat) : Nat

Return the second argument, ignoring an erased (usage-0) Nat tag that only takes part in type checking.

proofIrrelevantWitnessZero

def proofIrrelevantWitnessZero : Nat

A use of proofIrrelevantTag with tag zero, evaluating to one.

proofIrrelevantWitnessSucc

def proofIrrelevantWitnessSucc : Nat

A use of proofIrrelevantTag with tag one, evaluating to one; it is interchangeable with the zero-tag use under proof irrelevance.

Nat.beqSym

def Nat.beqSym (a : Nat) (b : Nat) : Nat.beq a b = Nat.beq b a

Boolean equality on natural numbers is symmetric: Nat.beq a b = Nat.beq b a.

Nat.bleRefl

def Nat.bleRefl (n : Nat) : Nat.ble n n = true

Boolean less-than-or-equal on natural numbers is reflexive: Nat.ble n n = true.

List.mapComp

def List.mapComp {A B : Type} {C : Type} (f : A -> B) (g : B -> C) (xs : List A) : map g (map f xs) = map (fun (x : A) => g (f x)) xs

Mapping twice is mapping the composition: map g (map f xs) = map (g ∘ f) xs.

List.zipWith

def List.zipWith {A B : Type} {C : Type} (f : A -> B -> C) (xs : List A) (ys : List B) : List C

Combine two lists elementwise with a function, stopping at the shorter one.

Option.toList

def Option.toList (A : Type) (mx : Option A) : List A

Convert a Maybe to a list of zero or one elements.

decToBool

def decToBool {P : Type} (d : Dec P) : Bool

Forget a decision procedure’s evidence, keeping only whether it answered yes.

tfCode

def tfCode (b : Bool) : Type

Send true to Unit and false to Empty; used to tell true and false apart.

trueNeFalse

def trueNeFalse (p : true = false) : Empty

True is not false: a path true = false yields Empty.

Bool.boolInspect

def Bool.boolInspect (b : Bool) (P : Bool -> Type) : (b = true -> P true) -> (b = false -> P false) -> P b

Case analysis on a boolean that also remembers which value it is (Agda’s inspect pattern).

Nat.bltSuccR

def Nat.bltSuccR (x : Nat) (n : Nat) (h : Nat.blt x n = true) : Nat.blt x (succ n) = true

A strict upper bound can be raised by one: x < n implies x < n + 1.

Nat.bltSelfSucc

def Nat.bltSelfSucc (m : Nat) : Nat.blt m (succ m) = true

Every natural number is strictly less than its successor: m < m + 1.

Nat.bltZeroAbsurd

def Nat.bltZeroAbsurd {A : Type} (m : Nat) (h : Nat.blt m zero = true) : A

Nothing is below zero: a proof of m < 0 eliminates into any type (the base case of termination_by).

Nat.subLtSucc

def Nat.subLtSucc (m : Nat) (x : Nat) : Nat.blt (sub m x) (succ m) = true

Truncated subtraction stays below the successor: m - x < m + 1.

subLt

def subLt (m : Nat) (k : Nat) (j : Nat) (h : Nat.blt m (succ k) = true) (e : Nat.blt m (succ j) = false) : Nat.blt (sub m (succ j)) k = true

If m < k + 1 and not m < j + 1, then m - (j + 1) < k.

Nat.modAuxStep

def Nat.modAuxStep (c : Bool) (m : Nat) (k : Nat) (j : Nat) : Nat

The shape of modAuxFuel after one step, branching on whether m < j + 1; a proof helper for modAuxLt.

Nat.modAuxLt

def Nat.modAuxLt (k : Nat) : (m : Nat) -> (j : Nat) -> Nat.blt m k = true -> Nat.blt (modAuxFuel k m (succ j)) (succ j) = true

With enough fuel (m < k), the remainder computed by modAuxFuel is less than the divisor j + 1.

Nat.modLt

def Nat.modLt (m : Nat) (n : Nat) : Nat.blt (Nat.mod m (succ n)) (succ n) = true

The remainder modulo n + 1 is less than n + 1.

Nat.subAddCancel

def Nat.subAddCancel (n : Nat) : (m : Nat) -> Nat.blt m n = false -> add n (sub m n) = m

Subtracting and adding back cancels when n <= m: n + (m - n) = m.

Nat.addRotate

def Nat.addRotate (n : Nat) (x : Nat) (s : Nat) : add (add n x) s = add x (add n s)

Moving the first summand inward: (n + x) + s = x + (n + s).

Nat.divAuxStep

def Nat.divAuxStep (c : Bool) (k : Nat) (q : Nat) (m : Nat) (j : Nat) : Nat

The shape of divAuxFuel after one step, branching on whether m < j + 1; a proof helper for divModAuxEq.

Nat.divModStepEq

def Nat.divModStepEq (c : Bool) (k : Nat) (q : Nat) (m : Nat) (j : Nat) : Type

The statement of divModAuxEq after one step; a proof helper.

Nat.divModAuxEq

def Nat.divModAuxEq (f : Nat) : (q : Nat) -> (m : Nat) -> (j : Nat) -> add (mul (divAuxFuel f q m (succ j)) (succ j)) (modAuxFuel f m (succ j)) = add (mul q (succ j)) m

The division invariant of the fuelled helpers, for any fuel: quotient × divisor + remainder = q × divisor + m.

Nat.divModEq

def Nat.divModEq (m : Nat) (j : Nat) : add (mul (Nat.div m (succ j)) (succ j)) (Nat.mod m (succ j)) = m

Division with remainder: (m / (j + 1)) × (j + 1) + m mod (j + 1) = m.

Nat.bltTrans

def Nat.bltTrans (m n p : Nat) (h1 : Nat.blt m n = true) (h2 : Nat.blt n p = true) : Nat.blt m p = true

Transitivity of the strict boolean order Nat.blt on natural numbers.

Nat.bltPredL

def Nat.bltPredL (m : Nat) (n : Nat) (h : Nat.blt (succ m) n = true) : Nat.blt m n = true

Dropping one from the left of a strict bound: m + 1 < n implies m < n.

Nat.bleSuccR

def Nat.bleSuccR (a : Nat) (c : Nat) (h : Nat.ble a c = true) : Nat.ble a (succ c) = true

Raising a bound by one: a <= c implies a <= c + 1.

Nat.bleSuccL

def Nat.bleSuccL (a : Nat) (c : Nat) (h : Nat.ble (succ a) c = true) : Nat.ble a c = true

Dropping one from the left of a bound: a + 1 <= c implies a <= c.

Nat.bleAddL

def Nat.bleAddL (a : Nat) (b : Nat) (c : Nat) (h : Nat.ble (add a b) c = true) : Nat.ble a c = true

The left summand of a bounded sum is bounded: a + b <= c implies a <= c.

Nat.bleAddR

def Nat.bleAddR (a : Nat) (b : Nat) (c : Nat) (h : Nat.ble (add a b) c = true) : Nat.ble b c = true

The right summand of a bounded sum is bounded: a + b <= c implies b <= c.

Nat.addPosL

def Nat.addPosL (x : Nat) (y : Nat) (hx : Nat.blt 0 x = true) : Nat.blt 0 (add x y) = true

A sum with a positive left summand is positive: 0 < x implies 0 < x + y.

Nat.powTwoPos

def Nat.powTwoPos (k : Nat) : Nat.blt 0 (Nat.pow 2 k) = true

Every power of two is positive: 0 < 2 ^ k.

IsTrue

data IsTrue : Bool -> Type

IsTrue b: the Boolean b computes to true. Use it for preconditions written as Boolean expressions (it needs no elimination of Eq); prove it for a concrete value with isTrue.

IsTrue.toEq

def toEq {b : Bool} (h : IsTrue b) : Eq Bool b true

The truth of a Boolean as an equality.

IsTrue.ofEq

def ofEq {b : Bool} (h : Eq Bool b true) : IsTrue b

An equality with true as the truth of a Boolean.

Bool.falseNeTrue

def falseNeTrue (h : Eq Bool false true) : Empty

false and true are different.

DecEq

def DecEq (A : Type) : Type

A 的相等可判定：任兩個值，x = y 成立或不成立（同 Lean 的 DecidableEq）。 路徑版是 foundations 的 isDiscrete（給 Hedberg）；DecEq.toDiscrete（hlevel）由這個轉過去。

Nat.succInj

def succInj {m : Nat} {n : Nat} (h : Eq Nat (succ m) (succ n)) : Eq Nat m n

succ is injective.

Path.cong

def Path.cong {l : Level} {m : Level} {A : Type l} {B : Type m} {a : A} {b : A} (p : a ≡ b) (f : A -> B) : f a ≡ f b

Applies f to both ends of a path: p.cong(f) runs from f a to f b.