Cyril Cohen has marked this topic as unresolved.
This topic was moved here from #Coq users > Struggle with using canonical structures mathcomp style by Cyril Cohen.
This topic was moved to #math-comp users > Struggle with using canonical structures mathcomp style by Cyril Cohen.
I blindly followed the suggestion to move this to #math-comp users but it has nothing to do with mathcomp. It's a Coq bug... So I'm moving it back.
This topic was moved here from #math-comp users > Struggle with using canonical structures mathcomp style by Cyril Cohen.
Here are three workarounds:
Structure type := Pack{
MT: Type;
ops: MT * unit;
lms: ops = ops;
}.
(* Call already defined projections *)
Definition emtpy1 (e : type) : MT e := (ops e).1.
(* Call & reduce already defined projections *)
Definition emtpy2 (e : type) : MT e := Eval cbv [ops fst] in (ops e).1.
(* Decompile deep pattern matching manually *)
Definition empty3 (e : type) : MT e :=
match e with {| ops := x |} => match x with (o, _) => o end end.
given that this is a bug, should I open an issue on github ?
I opened https://github.com/coq/coq/issues/16749
Last updated: Jan 31 2023 at 14:03 UTC