Built with Alectryon, running Coq+SerAPI v8.16.0+0.16.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
From Tealeaves Require Export
Examples.STLC.Syntax
Simplification.Tests.Support.Import STLC.Syntax.TermNotations.Ltacsimplify_extract :=
first [ change ((?f ∘ extract) (?dec, ?var)) with (f var)
| change ((?g ∘ (?f ∘ extract)) (?dev, ?var)) with ((g ∘ f) var)
].Ltacsimplify_map_ret :=
change ((map ret ∘ ?f) ?leaf) with (map ret (f leaf));
rewrite map_to_ap.Ltacsimplify_ret :=
change ((ret ∘ ?f) ?leaf) with (ret (f leaf)).Ltacsimplify_leaf :=
try simplify_extract;
try simplify_map_ret;
try simplify_ret;
unfold_all_transparent_tcs.(** * Simplification tests for categorical operations *)(******************************************************************************)Sectiontest.Context (G: Type -> Type) `{Mult G} `{Map G} `{Pure G}
`{Applicative G} (v1 v2: Type).Implicit Types (tbody: Lam v1) (v: v1) (τ: typ).Generalizable Variablest v τ body.(** ** <<binddt>> and <<ret>> *)(******************************************************************************)Sectionbinddt_ret.(* Interestingly, these goals won't be accepted even if we add Generalizable Variable f. Implicit Type (f: nat * v1 -> G (Lam v2)). I think because binddt is typechecked before the universal generalization of f affects anything *)Context (f: nat * v1 -> G (Lam v2)).
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
binddt f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
binddt f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
f (Ƶ, v) = f (Ƶ, v)
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
f (Ƶ, v) = f (0, v)
reject.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
binddt f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
f (0, v) = f (Ƶ, v)
reject.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
f (0, v) = f (0, v)
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
binddt f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
f (Ƶ, v) = f (Ƶ, v)
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
f (Ƶ, v) = f (0, v)
reject.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = binddt f (tvar v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = binddt f (tvar v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
binddt f (ret v) = binddt f (tvar v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
binddt f (ret v) = binddt f (tvar v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallv, binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
binddt f (ret v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
f (Ƶ, v) = f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2) v: v1
f (Ƶ, v) = f (Ƶ : nat, v)
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallt1t2,
binddt f (⟨ t1 ⟩ (t2)) =
pure (app (V:=v2)) <⋆> binddt f t1 <⋆> binddt f t2
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallt1t2,
binddt f (⟨ t1 ⟩ (t2)) =
pure (app (V:=v2)) <⋆> binddt f t1 <⋆> binddt f t2
test.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallτbody,
binddt f ((λ) τ body) =
pure ((λ) τ) <⋆> binddt (f ⦿ 1) body
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G (Lam v2)
forallτbody,
binddt f ((λ) τ body) =
pure ((λ) τ) <⋆> binddt (f ⦿ 1) body
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2
forallv, bindd f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2
forallv, bindd f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2 v: v1
bindd f (ret v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2 v: v1
f (Ƶ, v) = f (Ƶ, v)
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2
forallv, bindd f (tvar v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2
forallv, bindd f (tvar v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2 v: v1
bindd f (tvar v) = f (Ƶ, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2 v: v1
f (Ƶ, v) = f (Ƶ, v)
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2
forallt1t2,
bindd f (⟨ t1 ⟩ (t2)) = (⟨ bindd f t1 ⟩ (bindd f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2
forallt1t2,
bindd f (⟨ t1 ⟩ (t2)) = (⟨ bindd f t1 ⟩ (bindd f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2 t1, t2: Lam v1
bindd f (⟨ t1 ⟩ (t2)) = (⟨ bindd f t1 ⟩ (bindd f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2 t1, t2: Lam v1
(⟨ bindd f t1 ⟩ (bindd f t2)) =
(⟨ bindd f t1 ⟩ (bindd f t2))
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2 τ: typ body: Lam v1
bindd f ((λ) τ body) = (λ) τ (bindd (f ⦿ 1) body)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> Lam v2 τ: typ body: Lam v1
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2
forallv, bind f (ret v) = f v
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2
forallv, bind f (ret v) = f v
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2 v: v1
bind f (ret v) = f v
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2 v: v1
bind f (ret v) = f v
Abort.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2
forallv, bind f (tvar v) = f v
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2
forallv, bind f (tvar v) = f v
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2 v: v1
bind f (tvar v) = f v
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2 v: v1
f v = f v
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2
forallt1t2,
bind f (⟨ t1 ⟩ (t2)) = (⟨ bind f t1 ⟩ (bind f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2
forallt1t2,
bind f (⟨ t1 ⟩ (t2)) = (⟨ bind f t1 ⟩ (bind f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2 t1, t2: Lam v1
bind f (⟨ t1 ⟩ (t2)) = (⟨ bind f t1 ⟩ (bind f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2 t1, t2: Lam v1
(⟨ bind f t1 ⟩ (bind f t2)) =
(⟨ bind f t1 ⟩ (bind f t2))
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2
forallτbody,
bind f ((λ) τ body) = (λ) τ (bind f body)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2
forallτbody,
bind f ((λ) τ body) = (λ) τ (bind f body)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2 τ: typ body: Lam v1
bind f ((λ) τ body) = (λ) τ (bind f body)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> Lam v2 τ: typ body: Lam v1
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2
forallv, mapdt f (ret v) = pure ret <⋆> f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2
forallv, mapdt f (ret v) = pure ret <⋆> f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2 v: v1
mapdt f (ret v) = pure ret <⋆> f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2 v: v1
(map ret ∘ f) (Ƶ, v) = pure ret <⋆> f (0, v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2 v: v1
pure (tvar (V:=v2)) <⋆> f (0, v) =
pure (tvar (V:=v2)) <⋆> f (0, v)
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2
forallt1t2,
mapdt f (⟨ t1 ⟩ (t2)) =
pure (app (V:=v2)) <⋆> mapdt f t1 <⋆> mapdt f t2
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2
forallt1t2,
mapdt f (⟨ t1 ⟩ (t2)) =
pure (app (V:=v2)) <⋆> mapdt f t1 <⋆> mapdt f t2
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2 t1, t2: Lam v1
mapdt f (⟨ t1 ⟩ (t2)) =
pure (app (V:=v2)) <⋆> mapdt f t1 <⋆> mapdt f t2
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2 t1, t2: Lam v1
pure (app (V:=v2)) <⋆> mapdt f t1 <⋆> mapdt f t2 =
pure (app (V:=v2)) <⋆> mapdt f t1 <⋆> mapdt f t2
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2
forallτbody,
mapdt f ((λ) τ body) =
pure ((λ) τ) <⋆> mapdt (f ⦿ 1) body
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2
forallτbody,
mapdt f ((λ) τ body) =
pure ((λ) τ) <⋆> mapdt (f ⦿ 1) body
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2 τ: typ body: Lam v1
mapdt f ((λ) τ body) =
pure ((λ) τ) <⋆> mapdt (f ⦿ 1) body
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> G v2 τ: typ body: Lam v1
pure ((λ) τ) <⋆> mapdt (f ⦿ 1) body =
pure ((λ) τ) <⋆> mapdt (f ⦿ 1) body
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2
forallv, mapd f (ret v) = ret (f (0, v))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2
forallv, mapd f (ret v) = ret (f (0, v))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2 v: v1
mapd f (ret v) = ret (f (0, v))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2 v: v1
(ret ∘ f) (Ƶ, v) = ret (f (0, v))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2 v: v1
tvar (f (0, v)) = tvar (f (0, v))
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2
forallt1t2,
mapd f (⟨ t1 ⟩ (t2)) = (⟨ mapd f t1 ⟩ (mapd f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2
forallt1t2,
mapd f (⟨ t1 ⟩ (t2)) = (⟨ mapd f t1 ⟩ (mapd f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2 t1, t2: Lam v1
mapd f (⟨ t1 ⟩ (t2)) = (⟨ mapd f t1 ⟩ (mapd f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2 t1, t2: Lam v1
(⟨ mapd f t1 ⟩ (mapd f t2)) =
(⟨ mapd f t1 ⟩ (mapd f t2))
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2 τ: typ body: Lam v1
mapd f ((λ) τ body) = (λ) τ (mapd (f ⦿ 1) body)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: nat * v1 -> v2 τ: typ body: Lam v1
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2
forallv, map f (ret v) = ret (f v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2
forallv, map f (ret v) = ret (f v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2 v: v1
map f (ret v) = ret (f v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2 v: v1
(ret ∘ (f ∘ extract)) (Ƶ, v) = ret (f v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2 v: v1
tvar ((f ∘ snd) (0, v)) = tvar (f v)
reflexivity.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2
forallv, map f (tvar v) = tvar (f v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2
forallv, map f (tvar v) = tvar (f v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2 v: v1
map f (tvar v) = tvar (f v)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2 v: v1
(ret ∘ (f ∘ extract)) (Ƶ, v) = tvar (f v)
reflexivity.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2
forallt1t2,
map f (⟨ t1 ⟩ (t2)) = (⟨ map f t1 ⟩ (map f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2
forallt1t2,
map f (⟨ t1 ⟩ (t2)) = (⟨ map f t1 ⟩ (map f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2 t1, t2: Lam v1
map f (⟨ t1 ⟩ (t2)) = (⟨ map f t1 ⟩ (map f t2))
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2 t1, t2: Lam v1
(⟨ map f t1 ⟩ (map f t2)) = (⟨ map f t1 ⟩ (map f t2))
conclude.Qed.
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2
forallτbody, map f ((λ) τ body) = (λ) τ (map f body)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2
forallτbody, map f ((λ) τ body) = (λ) τ (map f body)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2 τ: typ body: Lam v1
map f ((λ) τ body) = (λ) τ (map f body)
G: Type -> Type H: Mult G H0: Map G H1: Pure G Map_G: Map G Pure_G: Pure G Mult_G: Mult G H2: Applicative G v1, v2: Type f: v1 -> v2 τ: typ body: Lam v1