Object operators

at

(at k o)

(at k o)

• takes k: string
• takes o: object
• produces a

(at i l)

(at i l)

• takes i: integer
• takes o: list
• produces bool

projection

Supported in either invariants or properties.

+

(+ x y)

(+ x y)

• takes x: object
• takes y: object
• produces object

Object merge

Supported in either invariants or properties.

drop

(drop keys o)

(drop keys o)

• takes keys: [string]
• takes o: object
• produces object

drop entries having the specified keys from an object

Supported in either invariants or properties.

take

(take keys o)

(take keys o)

• takes keys: [string]
• takes o: object
• produces object

take entries having the specified keys from an object

Supported in either invariants or properties.

length

(length o)

(length o)

• takes o: object
• produces integer

the number of key-value pairs in the object

Supported in either invariants or properties.