blob: e433f158e487c79969a8877030dce8fc06b3b7c5 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Require Import EquivDec List.
Generalizable All Variables.
Program Definition list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq :=
(fun (x y : list A) => _).
Admit Obligations of list_eqdec.
Program Definition list_eqdec' `(eqa : EqDec A eq) : EqDec (list A) eq :=
(fun _ : nat => (fun (x y : list A) => _)) 0.
Admit Obligations of list_eqdec'.
|
