diff --git a/flake.nix b/flake.nix
index 20583da..7f6c705 100644
--- a/flake.nix
+++ b/flake.nix
@@ -26,6 +26,7 @@
           shellHook = ''
             echo "Entering Nix shell with Lean and VS Code..."
             export PS1="\[\e[1;32m\][nix-shell:\w]$\[\e[m\] "
+            export PATH="$PWD/.lake/build/bin:$PATH"
           '';
         };
     in
diff --git a/src/Ep133.lean b/src/Ep133.lean
index e69de29..a016816 100644
--- a/src/Ep133.lean
+++ b/src/Ep133.lean
@@ -0,0 +1,4 @@
+
+import Ep133.Parsing
+import Ep133.Types
+import Ep133.Util
diff --git a/src/Ep133/Parsing.lean b/src/Ep133/Parsing.lean
new file mode 100644
index 0000000..f78bdc3
--- /dev/null
+++ b/src/Ep133/Parsing.lean
@@ -0,0 +1,112 @@
+
+import Ep133.Types
+import Ep133.Util
+
+
+open Ep133.Types
+open Ep133.Util (getFloat32BE getUInt32 require)
+
+open ParseResult (throw)
+
+
+-- See <https://github.com/phones24/ep133-export-to-daw/blob/99454368f8da44b8b5bf495df0f89c72603b8dc4/docs/EP133_FORMATS.md> for reference.
+
+namespace Ep133.Parsing
+
+
+def parseEffects (raw : ByteArray) : ParseResult Effects :=
+  do
+   require (raw.size >= 100)
+      $ throw ("Effects only contains " ++ toString raw.size ++ " bytes.")
+    let effectType := raw[4]!
+    let active ← EffectLabel.ofUInt8 effectType
+    let effects ←
+      (List.range 7).mapM
+        (fun i ↦
+          do
+            let label ← EffectLabel.ofUInt8 i.toUInt8
+            let param1 := getFloat32BE raw $ 8 + 4 * i
+            let param2 := getFloat32BE raw $ 72 + 4 * i
+            pure ⟨ label , {param1, param2} ⟩
+        )
+    pure
+      {
+        raw
+      , active
+      , effects := Std.HashMap.ofList effects
+      }
+
+
+def makePatternLabel (l : Fin 4) (n : UInt8) : ParseResult PatternLabel :=
+  do
+    require (n > 0 && n < 100)
+      $ throw ("Pattern " ++ toString n ++ " is out of range.")
+    pure {letter := l, number := Fin.ofNat 99 $ n.toNat - 1}
+
+
+def parseScene (raw : ByteArray) (offset : Nat) : ParseResult Scene :=
+  do
+    let patternA ← makePatternLabel 0 $ raw[offset + 0]!
+    let patternB ← makePatternLabel 1 $ raw[offset + 1]!
+    let patternC ← makePatternLabel 2 $ raw[offset + 2]!
+    let patternD ← makePatternLabel 3 $ raw[offset + 3]!
+    pure
+      {
+        patternA, patternB, patternC, patternD
+      , timeSignature := {numerator := raw[offset + 4]!.toNat, denominator := raw[offset + 5]!.toNat}
+      }
+
+
+def parseScenes (raw : ByteArray) : ParseResult Scenes :=
+  do
+    require (raw.size >= 605)
+      $ throw ("Scenes only contains " ++ toString raw.size ++ " bytes.")
+    let sceneCount := raw[604]! |> UInt8.toNat
+    let scenes : List Scene ← (List.range sceneCount).mapM (fun n ↦ parseScene raw (1 + 6 * n))
+    pure
+      {
+        raw
+      , scenes := scenes.toArray
+      }
+
+
+def parsePad (raw : ByteArray) : ParseResult Pad :=
+  do
+    require (raw.size = 26)
+      $ throw ("Pad contains " ++ toString raw.size ++ " bytes instead of 27.")
+    let playMode ← PlayMode.ofUInt8 raw[23]!
+    let volume ← Volume.ofUInt8 raw[16]!
+    let timeStretchMode ← TimeStretchMode.ofUInt8 raw[21]!
+    let timeStretchBars ← TimeStretchBars.ofUInt8 raw[25]!
+    let chokeGroup ← ChokeGroup.ofUInt8 raw[22]!
+    let soundId ← SoundId.ofUInt8s raw[2]! raw[1]!
+    let pan ← Pan.ofUInt8 raw[18]!
+    let trim :=
+      {
+        left := getUInt32 0 raw[6]! raw[5]! raw[4]! |> UInt32.toNat
+        right := getUInt32 0 raw[10]! raw[9]! raw[8]! |> UInt32.toNat
+      }
+    let pitch ← Pitch.ofUInt8s raw[17]! 0  -- raw[26]!
+    pure
+      {
+        raw
+      , soundId
+      , volume
+      , attack := raw[19]!
+      , release := raw[20]!
+      , playMode
+      , timeStretch :=
+          {
+            mode := timeStretchMode
+          , bars:= timeStretchBars
+          , bpm := getFloat32BE raw 12
+          }
+      , pitch
+      , trim
+      , pan
+      , chokeGroup
+      , midiChannel := raw[3]!
+      }
+
+
+end Ep133.Parsing
diff --git a/src/Ep133/Types.lean b/src/Ep133/Types.lean
new file mode 100644
index 0000000..92b1b55
--- /dev/null
+++ b/src/Ep133/Types.lean
@@ -0,0 +1,375 @@
+
+import Ep133.Util
+import Lean.Data.Json.FromToJson
+import Std.Data.HashMap.Basic
+import Std.Data.TreeMap.Raw.Basic
+
+open Ep133.Util (require)
+open Lean (Json ToJson)
+
+namespace Ep133.Types
+
+
+private instance : Repr ByteArray where
+  reprPrec := reprPrec ∘ ByteArray.toList
+
+
+inductive ParseResult (a : Type) where
+| parsed : a → ParseResult a
+| throw : String → ParseResult a
+deriving Repr, BEq
+open ParseResult (throw)
+
+instance : Monad ParseResult where
+  pure := ParseResult.parsed
+  bind
+  | ParseResult.parsed x, f => f x
+  | ParseResult.throw s, _ => ParseResult.throw s
+
+instance : Alternative ParseResult where
+  failure := ParseResult.throw "Parsing failed."
+  orElse
+  | ParseResult.parsed x, _ => ParseResult.parsed x
+  | ParseResult.throw _, f => f ()
+
+
+inductive EffectLabel where
+| OFF
+| DLY
+| RVB
+| DST
+| CXO
+| FLT
+| CMP
+deriving Repr, BEq, Hashable, ToJson
+
+instance : ToString EffectLabel where
+  toString
+  | EffectLabel.OFF => "OFF"
+  | EffectLabel.DLY => "DLY"
+  | EffectLabel.RVB => "RVB"
+  | EffectLabel.DST => "DST"
+  | EffectLabel.CXO => "CXO"
+  | EffectLabel.FLT => "FLT"
+  | EffectLabel.CMP => "CMP"
+
+namespace EffectLabel
+
+  def ofUInt8 : UInt8 → ParseResult EffectLabel
+  | 0 => pure OFF
+  | 1 => pure DLY
+  | 2 => pure RVB
+  | 3 => pure DST
+  | 4 => pure CXO
+  | 5 => pure FLT
+  | 6 => pure CMP
+  | i => throw $ "Effect " ++ toString i ++ " is not defined."
+
+end EffectLabel
+
+
+structure EffectParams where
+  param1 : Float
+  param2 : Float
+deriving Repr, BEq, ToJson
+
+
+structure Effects where
+  raw : ByteArray
+  active : EffectLabel
+  effects : Std.HashMap EffectLabel EffectParams
+deriving Repr
+
+instance : ToJson Effects where
+  toJson x :=
+    open Lean.ToJson (toJson) in
+    ToJson.toJson
+      $ Json.mkObj
+      [
+        ⟨ "active" , toJson x.active ⟩
+      , ⟨ "effects", Json.mkObj $ x.effects.toList.map (fun ⟨ k , v ⟩ ↦ ⟨ toString k , toJson v ⟩) ⟩
+      ]
+
+
+structure TimeSignature where
+  numerator : Nat
+  denominator : Nat
+deriving Repr, BEq
+
+instance : ToString TimeSignature where
+  toString x := toString x.numerator ++ "/" ++ toString x.denominator
+
+instance : ToJson TimeSignature where
+  toJson := ToJson.toJson ∘ toString
+
+
+structure PatternLabel where
+  letter : Fin 4
+  number : Fin 99
+deriving Repr, BEq
+
+instance : ToString PatternLabel where
+  toString
+  | ⟨ l , n ⟩ =>
+    let letter := l.toNat + 'A'.toNat |> Char.ofNat
+    let number := if n.toNat < 9 then "0" ++ toString (n.toNat + 1) else toString (n.toNat + 1)
+    letter.toString ++ number
+
+instance : ToJson PatternLabel where
+  toJson := ToJson.toJson ∘ toString
+
+
+structure Scene where
+  patternA : PatternLabel
+  patternB : PatternLabel
+  patternC : PatternLabel
+  patternD : PatternLabel
+  timeSignature : TimeSignature
+deriving Repr, BEq, ToJson
+
+instance : Inhabited Scene where
+  default :=
+    {
+      timeSignature := {numerator := 4, denominator := 4}
+    , patternA := {letter := 0, number := 0}
+    , patternB := {letter := 1, number := 0}
+    , patternC := {letter := 2, number := 0}
+    , patternD := {letter := 3, number := 0}
+    }
+
+
+structure Scenes where
+  raw : ByteArray
+  scenes : Array Scene
+deriving Repr, BEq
+
+instance : ToJson Scenes where
+  toJson := ToJson.toJson ∘ Scenes.scenes
+
+
+inductive TimeStretchMode where
+| OFF
+| BPM
+| BARS
+deriving Repr, BEq, ToJson
+
+namespace TimeStretchMode
+
+  def ofUInt8 : UInt8 → ParseResult TimeStretchMode
+  | 0 => pure OFF
+  | 1 => pure BPM
+  | 2 => pure BARS
+  | i => throw $ "Time stretch " ++ toString i ++ " is not defined."
+
+end TimeStretchMode
+
+
+inductive TimeStretchBars where
+| WHOLE
+| DOUBLE
+| QUADRUPLE
+| HALF
+| QUARTER
+deriving Repr, BEq, ToJson
+
+namespace TimeStretchBars
+
+  def ofUInt8 : UInt8 → ParseResult TimeStretchBars
+  | 0 => pure WHOLE
+  | 1 => pure DOUBLE
+  | 2 => pure QUADRUPLE
+  | 255 => pure HALF
+  | 254 => pure QUARTER
+  | i => throw $ "Time stretch bars " ++ toString i ++ " is not defined."
+
+end TimeStretchBars
+
+
+structure TimeStretch where
+  mode : TimeStretchMode
+  bars : TimeStretchBars
+  bpm : Float
+deriving Repr, BEq, ToJson
+
+
+inductive PlayMode where
+| ONE
+| KEY
+| LEG
+deriving Repr, BEq, ToJson
+
+namespace PlayMode
+
+  def ofUInt8 : UInt8 → ParseResult PlayMode
+  | 0 => pure ONE
+  | 1 => pure KEY
+  | 2 => pure LEG
+  | i => throw $ "Play mode " ++ toString i ++ " is not defined."
+
+end PlayMode
+
+
+inductive ChokeGroup where
+| TRUE
+| FALSE
+deriving Repr, BEq, ToJson
+
+namespace ChokeGroup
+
+  def ofUInt8 : UInt8 → ParseResult ChokeGroup
+  | 0 => pure TRUE
+  | 1 => pure FALSE
+  | i => throw $ "Choke group " ++ toString i ++ " is not defined."
+
+end ChokeGroup
+
+
+def Volume := Fin 201
+deriving Repr, BEq
+
+instance : ToJson Volume where
+  toJson := ToJson.toJson ∘ Fin.toNat
+
+namespace Volume
+
+  def ofUInt8 (i : UInt8) : ParseResult Volume :=
+    do
+      require (i <= 200)
+        $ throw ("Volume " ++ toString i ++ " is too large.")
+      pure $ Fin.ofNat 201 i.toNat
+
+end Volume
+
+
+structure Pitch where
+  integral : Fin 25
+  decimal : UInt8
+deriving Repr, BEq
+
+instance : ToString Pitch where
+  toString x := toString x.integral ++ "." ++ toString x.decimal
+
+instance : ToJson Pitch where
+  toJson := ToJson.toJson ∘ toString
+
+namespace Pitch
+
+  def ofUInt8s (i d : UInt8) : ParseResult Pitch :=
+    do
+      require (i <= 12 || i >= 244)
+        $ throw ("Pitch " ++ toString i ++ " is out of range.")
+      pure
+        {
+          integral := Fin.ofNat 25 $ if i <= 12 then i.toNat + 13 else 256 - i.toNat
+        , decimal := d
+        }
+
+end Pitch
+
+
+def SoundId := Fin 999
+deriving Repr, BEq
+
+instance : ToString SoundId where
+  toString i :=
+    let j := i.toNat + 1
+    if j < 10
+      then "00" ++ toString j
+      else if j < 99
+        then "0" ++ toString j
+        else toString j
+
+instance : ToJson SoundId where
+  toJson := ToJson.toJson ∘ toString
+
+namespace SoundId
+
+  def ofUInt8s (i j : UInt8) : ParseResult SoundId :=
+    do
+      let n := (i.toNat <<< 8) + j.toNat
+      require (n > 0 && n < 1000)
+        $ throw ("Sound ID " ++ toString n ++ " out of range.")
+      pure $ Fin.ofNat 999 (n - 1)
+
+end SoundId
+
+
+def Pan := Fin 33
+deriving Repr, BEq
+
+instance : ToString Pan where
+  toString i := (i.toNat.toFloat / 16 - 1) |> toString
+
+instance : ToJson Pan where
+  toJson i := ToJson.toJson (i.toNat.toFloat / 16 - 1)
+
+namespace Pan
+
+  def ofUInt8 (i : UInt8) : ParseResult Pan :=
+    do
+      require (i <= 16 || i >= 240)
+        $ throw ("Pan " ++ toString i ++ " is out of range.")
+      if i <= 16
+        then pure ∘ Fin.ofNat 33 $ i.toNat + 17
+        else pure ∘ Fin.ofNat 33 $ 255 - i.toNat
+
+end Pan
+
+
+
+structure Trim where
+  left : Nat
+  right : Nat
+deriving Repr, BEq, ToJson
+
+
+def Attack := UInt8
+deriving Repr, BEq
+
+instance : ToJson Attack where
+  toJson := ToJson.toJson ∘ UInt8.toNat
+
+
+def Release := UInt8
+deriving Repr, BEq
+
+instance : ToJson Release where
+  toJson := ToJson.toJson ∘ UInt8.toNat
+
+
+structure Pad where
+  raw : ByteArray
+  soundId : SoundId
+  volume : Volume
+  attack : Attack
+  release : Release
+  playMode : PlayMode
+  timeStretch : TimeStretch
+  pitch : Pitch
+  trim : Trim
+  pan : Pan
+  chokeGroup : ChokeGroup
+  midiChannel : UInt8
+deriving Repr, BEq
+
+instance : ToJson Pad where
+  toJson x :=
+    open Lean.ToJson (toJson) in
+    ToJson.toJson
+      $ Json.mkObj
+      [
+        ⟨ "soundId" , toJson x.soundId              ⟩
+      , ⟨ "volume"  , toJson x.volume               ⟩
+      , ⟨ "attack"  , toJson x.attack               ⟩
+      , ⟨ "release" , toJson x.release              ⟩
+      , ⟨ "playMode", toJson x.playMode             ⟩
+      , ⟨ "timeStretch", toJson x.timeStretch       ⟩
+      , ⟨ "pitch"      , toJson x.pitch             ⟩
+      , ⟨ "trim"       , toJson x.trim              ⟩
+      , ⟨ "pan"        , toJson x.pan               ⟩
+      , ⟨ "chokeGroup" , toJson x.chokeGroup        ⟩
+      , ⟨ "midiChannel", toJson x.midiChannel.toNat ⟩
+      ]
+
+
+end Ep133.Types
diff --git a/src/Ep133/Util.lean b/src/Ep133/Util.lean
new file mode 100644
index 0000000..57bf354
--- /dev/null
+++ b/src/Ep133/Util.lean
@@ -0,0 +1,26 @@
+
+namespace Ep133.Util
+
+
+def getFloat32BE (bytes : ByteArray) (offset : Nat) : Float :=
+  let getUInt32BE (bytes : ByteArray) (offset : Nat) : UInt32 :=
+    let b1 := bytes[offset    ]! |> UInt8.toUInt32
+    let b2 := bytes[offset + 1]! |> UInt8.toUInt32
+    let b3 := bytes[offset + 2]! |> UInt8.toUInt32
+    let b4 := bytes[offset + 3]! |> UInt8.toUInt32
+    (b1 <<< 24) ||| (b2 <<< 16) ||| (b3 <<< 8) ||| b4
+  Float32.toFloat ∘ Float32.ofBits $ getUInt32BE bytes offset
+
+
+def getUInt32 (i j k l : UInt8) : UInt32 :=
+  (i.toUInt32 <<< 24) + (j.toUInt32 <<< 16) + (k.toUInt32 <<< 8) + l.toUInt32
+
+
+def require {m : Type → Type} [Monad m] (cond : Bool) (action : m Unit) : m Unit :=
+  if cond then
+    pure ()
+  else
+    action
+
+
+end Ep133.Util
diff --git a/src/Ep133Test.lean b/src/Ep133Test.lean
index 4f2d2b5..6783ecd 100644
--- a/src/Ep133Test.lean
+++ b/src/Ep133Test.lean
@@ -1,4 +1,81 @@
 
+import Ep133
+
+
+open Ep133
+open Ep133.Types
+
+
+namespace Examples
+
+  def rawEffect : ByteArray :=
+    ByteArray.mk #[
+      0x00, 0x00, 0x00, 0x00,  0x00, 0x00, 0x00, 0x00,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x55, 0x3f
+    , 0x00, 0x00, 0x80, 0x3f,  0x00, 0x00, 0xbc, 0x3e,  0x00, 0x00, 0x1f, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x06, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x12, 0x3f,  0x00, 0x00, 0x80, 0x3f
+    , 0x00, 0x00, 0x80, 0x3f,  0x00, 0x00, 0x25, 0x3f,  0x00, 0x00, 0x2e, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x7b, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x00,  0x00, 0x00, 0x00, 0x00
+    ]
+
+  def rawScenes : ByteArray :=
+    ByteArray.mk #[
+      0x00, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x03, 0x03, 0x02, 0x02, 0x04, 0x04,  0x03, 0x04, 0x03, 0x03, 0x04, 0x04
+    , 0x05, 0x05, 0x04, 0x04, 0x04, 0x04,  0x02, 0x02, 0x05, 0x04, 0x04, 0x04,  0x07, 0x06, 0x06, 0x05, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x00, 0x00, 0x00, 0x04
+    , 0x00, 0x00, 0x00, 0x06, 0x00, 0x00, 0x00
+    ]
+
+  def rawPad : ByteArray :=
+    ByteArray.mk #[
+      0x00, 0x57, 0x01, 0x00,  0x00, 0x00, 0x00, 0x00,  0x11, 0x69, 0x00, 0x00,  0x00, 0x00, 0x00, 0x00
+    , 0x64, 0x00, 0x00, 0x00,  0xff, 0x00, 0x00, 0x00,  0x3c, 0x00
+    ]
+
+end Examples
+
+
+#guard (Effects.active <$> Parsing.parseEffects Examples.rawEffect) == ParseResult.parsed EffectLabel.OFF
+
+#guard ((Array.size ∘ Scenes.scenes) <$> Parsing.parseScenes Examples.rawScenes) == ParseResult.parsed 4
+
+#guard ((fun x ↦ x.scenes[0]!.timeSignature) <$> Parsing.parseScenes Examples.rawScenes) == ParseResult.parsed {numerator := 4, denominator := 4}
+
+
 def main (_args : List String) : IO UInt32 :=
   pure 0
-
diff --git a/src/Main.lean b/src/Main.lean
index c3ff52a..4752160 100644
--- a/src/Main.lean
+++ b/src/Main.lean
@@ -1,3 +1,78 @@
 
-def main (_args : List String) : IO UInt32 :=
-  pure 0
+import Cli
+import Ep133
+
+
+open Cli
+open Ep133.Parsing (parseEffects parsePad parseScenes)
+open Ep133.Types (ParseResult)
+open Lean (ToJson)
+
+
+def dump {α : Type} [ToJson α] (filepathFlag : String) (parse : ByteArray → ParseResult α) (p : Parsed) : IO UInt32 :=
+  do
+    let filepath : String := p.flag! filepathFlag |>.as! String
+    let raw ← IO.FS.readBinFile filepath
+    match parse raw with
+    | ParseResult.parsed x =>
+      IO.println (ToJson.toJson x).pretty
+      pure 0
+    | ParseResult.throw message =>
+      IO.println message
+      pure 1
+
+
+def dumpEffects : Parsed → IO UInt32 := dump "effects-file" parseEffects
+
+def dumpEffectsCmd := `[Cli|
+  "dump-effects" VIA dumpEffects;
+  "Dump the contents of effects."
+  FLAGS:
+    "effects-file" : String ; "The effects file."
+  EXTENSIONS:
+    defaultValues! #[
+      ("effects-file", "/dev/stdin")
+    ]
+]
+
+
+def dumpPad : Parsed → IO UInt32 := dump "pad-file" parsePad
+
+def dumpPadCmd := `[Cli|
+  "dump-pad" VIA dumpPad;
+  "Dump the contents of a pad."
+  FLAGS:
+    "pad-file" : String ; "The pad file."
+  EXTENSIONS:
+    defaultValues! #[
+      ("pad-file", "/dev/stdin")
+    ]
+]
+
+
+def dumpScene : Parsed → IO UInt32 := dump "scenes-file" parseScenes
+
+def dumpSceneCmd := `[Cli|
+  "dump-scenes" VIA dumpScene;
+  "Dump the contents of scenes."
+  FLAGS:
+    "scenes-file" : String ; "The scenes file."
+  EXTENSIONS:
+    defaultValues! #[
+      ("scenes-file", "/dev/stdin")
+    ]
+]
+
+
+def ep133 : Cmd := `[Cli|
+  ep133 NOOP; ["0.0.1"]
+  "Manipulate EP-133 K.O. II backup files."
+  SUBCOMMANDS:
+    dumpEffectsCmd;
+    dumpPadCmd;
+    dumpSceneCmd
+]
+
+
+def main (args : List String) : IO UInt32 :=
+  ep133.validate args