So This is follow for this thread:https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Strange.20behavior.20in.20.20Canonical.20structures/near/306677018

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Record operations (A B: eqType) (M: Type) := Operations {
Empty : M;
Lookup : A -> M -> option B;
}.
Structure type := Pack{
AT: eqType;
BT: eqType;
MT: Type;
ops: operations AT BT MT;
}.
Definition empty (e: type): (MT e) :=
let 'Pack _ _ _ (Operations x _):= e in x.
```

If I try to define a structure that depends on operations for specifying lemmas for those operations:

as follows:

```
Record lemmas (A B: eqType) (M: Type) (ops: operations A B M) := Lemmas {
Extensionality: forall m1 m2,
(forall i , Lookup ops i m1 = Lookup ops i m2) ->
m1 = m2
}.
Structure type := Pack{
AT: eqType;
BT: eqType;
MT: Type;
ops: operations AT BT MT;
lms: lemmas ops;
}.
Definition empty (e: type): (MT e) :=
let 'Pack _ _ _ (Operations x _) _:= e in x.
```

Coq rejects the definition of empty, it cannot unify `(MT e)`

with the type of the expression, even though it should have,

My main questions are how to fix it, and what would be the mathcomp idiomatic way of doing what I am trying to do, I tried reading code from mathcomp library but I got lost

This topic was moved to #Coq users > Struggle with using canonical structures mathcomp style by Cyril Cohen.

Last updated: Feb 08 2023 at 07:02 UTC