Require Export Autosubst_Basics.
Require Export Autosubst_MMap.
Require Export Autosubst_Classes.
Require Export Autosubst_Tactics.
Require Export Autosubst_Lemmas.
Require Export Autosubst_Derive.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

Set Implicit Arguments.

Section MMapInstances.

Variable (A B C : Type).
Variable (MMap_A_B : MMap A B).
Variable (MMap_A_C : MMap A C).
Variable (MMapLemmas_A_B : MMapLemmas A B).
Variable (MMapLemmas_A_C : MMapLemmas A C).
Variable (MMapExt_A_B : MMapExt A B).
Variable (MMapExt_A_C : MMapExt A C).

Global Instance MMap_option : MMap A (option B) := fun f ⇒ omap (mmap f).
Global Instance MMapLemmas_option : MMapLemmas A (option B).
Global Instance MMapExt_option : MMapExt A (option B).

Global Instance MMap_pair : MMap A (B × C).
Global Instance MMapLemmas_pair : MMapLemmas A (B × C).
Global Instance MMapExt_pair : MMapExt A (B × C).

Global Instance mmap_seq : MMap A (seq B) := fun f ⇒ map (mmap f).
Global Instance mmapLemmas_seq : MMapLemmas A (seq B).
Global Instance mmapExt_seq : MMapExt A (seq B).

Global Instance MMap_fun : MMap A (B → C) := fun f g x ⇒ mmap f (g x).

Global Instance MMapLemmas_fun : MMapLemmas A (B → C).

Global Instance MMapExt_fun : MMapExt A (B → C).

End MMapInstances.