Lines Matching refs:fld1
112 small_record = <| fld1 : num -> bool ; fld2 : num |>
115 val _ = Hol_datatype`squish_record = <|fld1:bool|>`
116 val _ = Hol_datatype`poly_squish_record = <|fld1:'a->'b|>`
121 `<| fld1 := SUC |>`
134 (``:(num,num)poly_squish_record``, [("fld1", ``SUC``)]) of
277 ("field sel. for fn type", ``r.fld1 x``, "r.fld1 x"),
279 ``r with fld1 := (\x. T)``, "r with fld1 := (\\x. T)"),
280 ("multi-field update", ``r with <| fld2 := 3; fld1 := x |>``,
281 "r with <|fld2 := 3; fld1 := x|>"),
322 ``<|fld1 := a very long expression indeed ;
324 "<|fld1 := a very long expression indeed;\n\
336 ``<| fld1 updated_by K t1 o K t2 |>``,
337 ``<| fld1 := t1 |>``)