Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

add_axiom

app

Build a function application f a.

app2

Build a function application f a b.

app3

Build a function application f a b c.

arrow

Build a non-dependent arrow A -> B.

bitvec_binop_ty

∀ {n : Nat}, BitVec n → BitVec n → BitVec n

bitvec_cmp_ty

∀ {n : Nat}, BitVec n → BitVec n → Bool

bitvec_getbit_ty

∀ {n : Nat}, BitVec n → Nat → Bool

bitvec_shift_ty

∀ {n : Nat}, BitVec n → Nat → BitVec n

bitvec_unop_ty

∀ {n : Nat}, BitVec n → BitVec n

bool_ty

Bool type.

build_bitvec_env

Build the BitVec environment, adding the BitVec type, operations, and theorems as axioms.

bvar

Bound variable.

bvx_ext_arith_shift_right_ty

Build BitVec.arithShiftRight : {n : Nat} → BitVec n → Nat → BitVec n.

bvx_ext_bveq

BV equality shorthand for bvar indices (a_idx, b_idx) under width bvar n_idx.

bvx_ext_concat_result

Concatenation result type helper: BitVec (Nat.add n m).

bvx_ext_count_zeros_ty

Build type for clz/ctz : {n : Nat} → BitVec n → Nat.

bvx_ext_ext_ty

Build ∀ {n} (a b : BitVec n), a = b ↔ (∀ i < n, getLsb a i = getLsb b i). Simplified as a Prop-valued type.

bvx_ext_fin2n

Build Fin (Nat.pow 2 n) type expression.

bvx_ext_forall_bv_nat

Build ∀ {n} (a : BitVec n) (k : Nat), P a k.

bvx_ext_forall_nat_bv

Build ∀ (n : Nat) (a : BitVec n), P n a.

bvx_ext_forall_one

Build ∀ {n} (a : BitVec n), P a.

bvx_ext_forall_three

Build ∀ {n} (a b c : BitVec n), P a b c.

bvx_ext_forall_two

Build ∀ {n} (a b : BitVec n), P a b — the standard two-bitvec quantifier.

bvx_ext_int

Build Int constant.

bvx_ext_nat

Build Nat constant.

bvx_ext_nateq

Nat equality Eq Nat lhs rhs.

bvx_ext_popcount_ty

Build type for popcount : {n : Nat} → BitVec n → Nat.

bvx_ext_reverse_ty

Build type for reverse : {n : Nat} → BitVec n → BitVec n.

bvx_ext_zero_extend_ty

Zero-extension type: {n : Nat} → (m : Nat) → BitVec n → BitVec m.

cst

Named constant with no universe levels.

int_ty

Int type.

mk_bitvec

Build BitVec n type expression.

mk_bitvec_add

Build BitVec.add a b (implicit n).

mk_bitvec_and

Build BitVec.and a b (implicit n).

mk_bitvec_mul

Build BitVec.mul a b (implicit n).

mk_bitvec_of_nat

Build BitVec.ofNat n val.

mk_bitvec_or

Build BitVec.or a b (implicit n).

mk_bitvec_sub

Build BitVec.sub a b (implicit n).

mk_bitvec_xor

Build BitVec.xor a b (implicit n).

mk_bitvec_zero

Build BitVec.zero n.

mk_bv_eq

Build Eq @{} (BitVec n) a b where n is a bvar.

mk_eq

Build Eq @{} ty a b.

mk_iff

Build Iff a b.

mk_nat_eq

Build Eq @{} Nat a b.

nat_ty

Nat type.

pi

Build Pi (name : dom), body with given binder info.

prop

Prop: Sort 0.

type1

Type 1: Sort 1.