## Stream: Equations devs & users

### Topic: Equations type error on `fin t` while `Program` does not

#### Lef Ioannidis (Mar 08 2022 at 16:04):

See this example of `Equations` raising a type error on an index mismatch of `fin` while `Program Definition` generates proof obligations. As far as I understand, the behavior should be to generate a proof obligation in both cases.

``````From Coq Require Import
Fin
List
Program.

From Equations Require Import
Equations.

Notation fin := t.

Equations list_replace{T}(l: list T)(i: fin (List.length l))(a: T): list T :=
list_replace (h::ts) F1 a := a :: ts;
list_replace (h::ts) (FS k) a := h :: list_replace ts k a.

Notation "v '@' i ':=' a" := (list_replace v i a) (at level 70).

Program Definition replace_twice{T}(l: list T)
(i j: fin (length l))(a: T): list T :=
let l' := l @ i := a in
l' @ j := a.

Fail Equations replace_twice{T}(l: list T)
(i j: fin (length l))(a: T): list T :=
replace_twice l i j a :=
let l' := l @ i := a in
l' @ j := a.
``````

#### Notification Bot (Mar 08 2022 at 16:04):

This topic was moved here from #Coq users > Equations type error on `fin t` while `Program` does not by Karl Palmskog.

#### James Wood (Mar 10 2022 at 14:09):

IIUC, to summarise, `Program` defers a failing judgemental equation as a propositional equality obligation, while `Equations` is not doing. I'm no expert, but it seems plausible to me that these are the two natural design choices for what each mechanism is trying to achieve (simply typed programs with `Prop` refinements vs dependently typed programs).

#### Yannick Forster (Mar 10 2022 at 14:53):

If you replace `l' @ j` by `l' @ _` then the `Equations` command generates the same obligation. I'm not sure I find this intuitive, but it works

Last updated: Jan 29 2023 at 15:02 UTC