mir-ikbch

Inductive term :=
  Tru
| Fls
| IfThenElse : term -> term -> term -> term.

Notation "'If' c1 'Then' c2 'Else' c3" := (IfThenElse c1 c2 c3)
(at level 200, right associativity, format
"'[v   ' 'If'  c1 '/' '[' 'Then'  c2  ']' '/' '[' 'Else'  c3 ']' ']'").

mir-ikbch

Set Implicit Arguments.

Inductive type : Type :=
| Nat : type
| Unit : type
| Func : type -> type -> type -> type -> type.

Notation "t / a --> s / b" := (Func t s a b) (at level 40, a at next level, s at next level).
  
Section Var.

mir-ikbch

Require Import List PeanoNat Arith Morphisms Setoid.
Import ListNotations.

Set Implicit Arguments.

Ltac optimize db :=
  eexists; intros;
  match goal with
    |- ?X = ?Y =>
    let P := fresh in

mir-ikbch

Require Import List PeanoNat.
Import ListNotations.
Set Universe Polymorphism.

Set Implicit Arguments.

Inductive t (eff : Type -> Type) (a : Type) :=
| Pure : a -> t eff a
| Eff : forall T, eff T -> (T -> t eff a) -> t eff a.