mapSize.key

Functions

mapSize

int mapSize ( Map ) ; defined in: mapSize.key Line: 16 Offset :4

Predicates

isFinite

isFinite ( Map ) ; defined in: mapSize.key Line: 20 Offset :4

Taclets

No choice condition specified

defIsFinite

defIsFinite { \schemaVar \variables any vx ; \schemaVar \variables int ix ; \schemaVar \variables Seq s ; \find ( isFinite ( m ) ) \varcond \replacewith ( \exists s ; ( \forall vx ; ( inDomain ( m , vx ) <-> ( \exists ix ; ( 0 <= ix & ix < seqLen ( s ) & seqGet <[ any ]> ( s , ix ) = vx ) ) ) ) ) };defined in: mapSize.key Line: 29 Offset :4

isFiniteOfMapEmpty