Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

add_axiom

Shorthand to add an axiom to env.

app

Function application f a.

app2

Function application f a b.

app3

Function application f a b c.

arr_ext_append_assoc_ty

Array.append_assoc : ∀ {α n m k}, Array α n → Array α m → Array α k → Prop

arr_ext_append_empty_left_ty

Array.append_empty_left : ∀ {α n}, Array α n → Prop

arr_ext_append_empty_right_ty

Array.append_empty_right : ∀ {α n}, Array α n → Prop

arr_ext_append_size_ty

Array.append_size : ∀ {α n m}, Array α n → Array α m → Prop

arr_ext_bind_assoc_ty

Array.bind_assoc : ∀ {α β γ n}, Array α n → (α → Array β n) → (β → Array γ n) → Prop

arr_ext_map_comp_ty

Array.map_comp : ∀ {α β γ n}, (β → γ) → (α → β) → Array α n → Prop

arr_ext_map_id_ty

Array.map_id : ∀ {α n}, Array α n → Prop

arr_ext_mergesort_ty

Array.mergesort : {α : Type} → {n : Nat} → [Ord α] → Array α n → Array α n

arr_ext_prefix_sum_ty

Array.prefix_sum : {α : Type} → {n : Nat} → Array α n → Array α n

arr_ext_pure_map_size_ty

Array.pure_map_size : ∀ {α β n}, (α → β) → Array α n → Prop

arr_ext_qsort_avg_ty

Array.qsort_average_case : ∀ {α n}, [Ord α] → Array α n → Prop

arr_ext_reverse_involution_ty

Array.reverse_involution : ∀ {α n}, Array α n → Prop

arr_ext_reverse_size_ty

Array.reverse_size : ∀ {α n}, Array α n → Prop

arr_ext_slice_ty

Array.slice : {α : Type} → {n : Nat} → Array α n → Nat → Nat → List α

arr_ext_sort_perm_ty

Array.sort_perm : ∀ {α n}, [Ord α] → Array α n → Prop

arr_ext_sort_sorted_ty

Array.sort_sorted : ∀ {α n}, [Ord α] → Array α n → Prop

arr_ext_sort_stable_ty

Array.sort_stable : ∀ {α n}, [Ord α] → Array α n → Prop

array_of

Array applied to element type and size.

arrow

Build a non-dependent arrow A -> B.

beq_of

BEq type class applied to a type.

bool_ty

Bool type constant.

build_array_env

Build Array type and all standard declarations, adding them to the environment.

default_pi

A default (explicit) Pi binder.

eq_expr

Build Eq @{} ty a b.

fin_of

Fin applied to a size argument.

implicit_pi

An implicit Pi binder.

inst_pi

An instance Pi binder [inst : ty].

list_of

List applied to a type argument.

mk_array_empty

Build Array.empty for a given element type (returns Array α 0).

mk_array_foldl

Build Array.foldl f init arr.

mk_array_get

Build Array.get arr idx.

mk_array_map

Build Array.map f arr.

mk_array_push

Build Array.push arr elem.

mk_array_set

Build Array.set arr idx val.

mk_array_tolist

Build Array.toList arr.

mk_array_ty

Build the Array α n type expression.

nat_add

Nat.add a b.

nat_min

Nat.min a b.

nat_sub

Nat.sub a b.

nat_succ

Nat.succ n — successor of a Nat expression.

nat_ty

Nat type constant.

option_of

Option applied to a type argument.

ord_of

Ord type class applied to a type.

prod_of

Prod applied to two type arguments.

prop

Prop: Sort 0.

type1

Type 1: Sort 1.