Lines Matching refs:fld1
304 (r with fld1 updated by val).fld2 = r.fld2
306 fld1 (fld2_fupd val r) = fld1 r
422 !r1 r2. (r1 = r2) = (r1.fld1 = r2.fld1) /\ (r1.fld2 = r2.fld2)
451 r1 with <| fld1 := v1 ; fld2 := v2 |> =
452 <| fld1 := v1; fld2 := v2 |>
457 !r. ?v1 v2 v3. r = <| fld1 := v1; fld2 := v2; fld3 := v3 |>
461 (!v1 v2 v3. P <| fld1 := v1; fld2 := v2; fld3 := v3 |>)
466 (<| fld1 := v11; fld2 := v21; fld3 := v31 |> =
467 <| fld1 := v12; fld2 := v22; fld3 := v32 |>) =