1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
From RecordUpdate Require Import RecordSet.
Require Import List.
Import ListNotations.
Import RecordSetNotations.
Module GH4.
Record foo := { a : bool ;
b : bool }.
Global Instance etaX_RtlExprs : Settable _ :=
settable!
Build_foo <a; b>.
Definition bar := {| a := true ; b := true |}.
Definition baz := bar<|a := false|>.
End GH4.
Definition l := [1; 2; 3].
Record foo := { a : list nat;
b : list bool; }.
#[export] Instance eta_foo : Settable _ := settable! Build_foo <a; b>.
Definition m_foo (x:foo) := x <| a := [1;2;3] |> <| b := [] |>.
|
