Example in Readme.md does not work as expected (set has wrong type - notations work fine)

[MSoegtropIMC]

The example given in Reade.md doesn't work as I would expect it. The function setAB' does what I think it should, but setAB has the wrong type - the a and b arguments have type nat->nat rather than nat:

From RecordUpdate Require Import RecordSet.

Record X := mkX { A: nat; B: nat; C: bool; }.

#[global]
Instance etaX : Settable _ := settable! mkX <A; B; C>.

Print set.

(* and now you can update fields! *)
Definition setAB a b x := set B b (set A a x).

Import RecordSetNotations.

Definition setAB' a b x := x <|A := a|> <|B := b|>.

Check setAB.

(* setAB : (nat -> nat) -> (nat -> nat) -> X -> X *)

Check setAB'.

(* setAB' : nat -> nat -> X -> X *)

[samuelgruetter]

In the case of setAB, a and b are not values, but "updater functions" that take in the old value as an argument. I also think that the readme is a bit confusing and would deserve better examples, maybe like this:

(* and now you can update fields! *)
Definition updateFields(x: X): X := set B (Nat.add 1) (set A (Nat.add 2) x).

(* you can also use a notation for the same thing: *)
Import RecordSetNotations.
Definition updateFields'(x: X): X := x <|A ::= Nat.add 2|> <|B ::= Nat.add 1|>.

(* Of course, you can also set them to a particular value that ignores the old value: *)
Definition setFields(x: X): X := set B (fun _ => 42) (set A (fun _ => 43) x).
Definition setFields'(x: X): X := x <|A := 43|> <|B := 42|>.

If/once I manage to cleanup my improvements (no more need for eta instances, OCaml-like update syntax and a simplifier) and turn them into a PR for this repo, I'll try to do a better job at explaining updaters vs setters, but in the meantime, I would guess @tchajed would also accept a PR to improve the explanations in the readme?

[tchajed]

Indeed the behavior is as intended but the README is admittedly confusing. It should explain that "setAB" is really updating both fields in terms of their old values, whereas setAB' is really setting to constants.

A PR against the README would be great! Please also copy the code to tests/ReadmeExampleTests.v so that we make sure it compiles.

[MSoegtropIMC]

I guessed that this are updater functions and actually use it - quite nice. So I agree that this is a documentation issue.