Stream: Coq users

Topic: Record Set and sub-records


view this post on Zulip 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!

view this post on Zulip Li-yao (Mar 13 2023 at 22:11):

r <| a ; x := v |>


Last updated: Jun 24 2024 at 13:02 UTC