Sha256: fb5eba1248b495aa284937771ce6c32f82dab8691bc3ad81050a87a3d3815340
Contents?: true
Size: 335 Bytes
Versions: 7
Compression:
Stored size: 335 Bytes
Contents
\* Create new pet
New_Pet( pet_input, id ) == [ id |-> id, name |-> pet_input.name, tag |-> pet_input.tag ]
(*
Copy all other fields from 'pet_input' expect Next_pet_id
{
CHOOSE p \in t_Pet :
p.id = Next_pet_id
/\ \A key \in DOMAIN pet_input.pet: p[key] = pet_input.pet[key]
};
*)
Version data entries
7 entries across 7 versions & 1 rubygems