Skip to main content Module obj Copy item path Source Abs Add ByInducFreeParamObj Cap Cart CartDim Choose ClosedRange Count Cup DefAlgoFreeParamObj DefHeaderFreeParamObj Div ExistFreeParamObj FamilyObj FiniteSeqListObj Literal [a, b, ...] as a finite sequence value (for membership in finite_seq(s, n)). FiniteSeqSet Set of functions fn(x N_pos: x <= n) s (Lit surface syntax: keyword finite_seq(s, n)). FnObj FnSet FnSetFreeParamObj ForallFreeParamObj Identifier IdentifierWithMod Intersect ListSet Log Real logarithm log(base, x) with base > 0, base != 1, x > 0. MatrixAdd MatrixListObj MatrixMul MatrixPow MatrixScalarMul MatrixSet MatrixSub Max Min Mod Mul Number ObjAtIndex Pow PowerSet ProductFreeParamObj ProductObj Proj Range SeqSet seq(s) — functions fn(x N_pos) s (no length bound; surface: keyword seq(s)).SetBuilder SetBuilderFreeParamObj SetDiff SetMinus Sub SumFreeParamObj SumObj Tuple TupleDim Union AtomObj 仅「名字/绑定子」的 Obj:: 的名字、与解析期自由参标记。 AtomicName FnObjHead Function-application head: plain identifier pieces or tagged free-parameter binders. Obj ParamObjType StandardSet fn_obj_to_string identifier_to_string identifier_with_mod_to_string obj_for_bound_param_in_scope Bound-parameter Objby stmts, coverage, etc.), matching parse-time ~kind tagging and Runtime::inst_obj param_binding_element_obj_for_store Element Obj~tag spine). strip_free_param_numeric_tags_in_display Removes ~ plus following ASCII digits everywhere (e.g. ~2aaa → aaa). Used on full
display JSON so every field is normalized; keeps ~ when not followed by digits (e.g. ~/). strip_parsing_free_param_tags_for_user_display