Set

Generated from the engine's own definition: compute-engine's symbol, which we neither extend nor document by hand. No examples yet — the crosswalk is the reason it has a page.

An unordered collection of distinct elements (a set).

FungrimSet↗

Set(any*) -> setas compute-engine declares it

Typed signatures

Type	Package	Applies
(any*) -> set	compute-engine	always

Domain: Compute engine

About

Crosswalk	Fungrim

Implementation

mappedmathlib4packages/oracle/src/mappings.ts

a Set is passed to Lean as a duplicate-free list of rationals, which is how the lane hands sets to Finset functions (they read it with List.toFinset); element order is not meaningful