Module functions

Expand description

Auto-generated module

🤖 Generated with SplitRS

Functions§

assoc_map_from_vec: Convert a Vec of pairs into an AssocMap.
build_hashmap_delete: Build HashMap.delete : {K V : Type} → K → HashMap K V → HashMap K V.
build_hashmap_env: Build HashMap type in the environment.
build_hashmap_extended: Build all HashMap operations into the environment.
build_hashmap_size: Build HashMap.size : {K V : Type} → HashMap K V → Nat.
count_matching: Count entries in an AssocMap matching a predicate.
hm_app: Application f a.
hm_app2: Application f a b.
hm_app3: Application f a b c.
hm_arrow: Non-dependent arrow A → B.
hm_bool: Bool.
hm_bvar: Bound variable.
hm_cst: Named constant.
hm_eq: Eq ty a b.
hm_ext_forall_map: ∀ {K V : Type}, HashMap K V → ... quantifier over a single map.
hm_ext_forall_map_k_v: Standard ∀ {K V} (m : HashMap K V) (k : K) (v : V) prefix.
hm_ext_forall_two_maps: ∀ {K V : Type}, HashMap K V → HashMap K V → ...
hm_ext_get_eq_none: Build HashMap.get m k = Option.none.
hm_ext_get_eq_some: Build HashMap.get m k = Option.some v equality.
hm_ext_map_eq: Equality of two HashMap K V values.
hm_list: List A.
hm_nat: Nat.
hm_option: Option V.
hm_pi: Pi binder.
hm_prop: Prop sort.
hm_ty: HashMap K V.
hm_type1: Type₁ sort.
hm_type2: Type₂ sort.
name_expr_map_from_iter: Build a NameExprMap from an iterator of (Name, Expr) pairs.

NameExprMap: A map from Name to Expr, backed by an association list.
StringMap: A map from String to arbitrary values, backed by an association list.