Rudy Peterson (Mar 13 2023 at 20:56): Rudy Peterson (Mar 13 2023 at 20:56):Hello!
I was wondering if it is possible to when using the RecordSet library on a record with a sub-record to set a sub-member without oo many nestings. Consider:
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.
Section Examples.
Variables X Y : Set.
Record A : Set :=
mk_A { x : X }.
Global Instance eta_A : Settable _ :=
settable! mk_A < x >.
Record B : Set :=
mk_B { a :> A; y : Y }.
Global Instance eta_B : Settable _ :=
settable! mk_B < a ; y >.
Definition set_x_A (v : X) (r : A) : A := r <| x := v |>.
Definition set_y_B (v : Y) (r : B) : B := r <| y := v |>.
Definition set_a_B (v : A) (r : B) : B := r <| a := v |>.
Fail Definition set_x_B1 (v : X) (r : B) : B := r <| x := v |>.
Definition set_x_B2 (v : X) (r : B) : B := r <| a := r <| x := v |> |>.
End Examples.
I would like to assign to the inner record as in set_x_B1 but that fails.
Is there a way to get around having to do nested assignments as in set_x_B2?
Thanks!
Li-yao (Mar 13 2023 at 22:11):r <| a ; x := v |>
Last updated: Oct 04 2023 at 19:01 UTC