LightAndLight

data Triple f a b c
  = Triple1 (f a) (f b) (f c)
  | Triple2 (f a) (f b) (f c)

data TripleAction a b c where
  Triple1Fst :: (a -> a) -> TripleAction a b c
  Triple1Snd :: (b -> b) -> TripleAction a b c
  Triple1Thd :: (c -> c) -> TripleAction a b c

LightAndLight

data Triple f a b c
  = Triple1 (f a) (f b) (f c)
  | Triple2 (f a) (f b) (f c)

data TripleAction a b c where
  Triple1Fst :: (a -> a) -> TripleAction a b c
  Triple1Snd :: (b -> b) -> TripleAction a b c
  Triple1Thd :: (c -> c) -> TripleAction a b c

LightAndLight

data Triple f a b c
  = Triple1 (f a) (f b) (f c)
  | Triple2 (f a) (f b) (f c)

data TripleAction a b c where
  Triple1Fst :: (a -> a) -> TripleAction a b c
  Triple1Snd :: (b -> b) -> TripleAction a b c
  Triple1Thd :: (c -> c) -> TripleAction a b c

LightAndLight

data Triple f a b c
  = Triple1 (f a) (f b) (f c)
  | Triple2 (f a) (f b) (f c)

data TripleAction a b c where
  Triple1Fst :: (a -> a) -> TripleAction a b c
  Triple1Snd :: (b -> b) -> TripleAction a b c
  Triple1Thd :: (c -> c) -> TripleAction a b c

LightAndLight

data Triple f a b c
  = Triple1 (f a) (f b) (f c)
  | Triple2 (f a) (f b) (f c)

data TripleAction a b c where
  Triple1Fst :: (a -> a) -> TripleAction a b c
  Triple1Snd :: (b -> b) -> TripleAction a b c
  Triple1Thd :: (c -> c) -> TripleAction a b c

LightAndLight

data Triple f a b c
  = Triple1 (f a) (f b) (f c)
  | Triple2 (f a) (f b) (f c)

data TripleAction a b c where
  Triple1Fst :: (a -> a) -> TripleAction a b c
  Triple1Snd :: (b -> b) -> TripleAction a b c
  Triple1Thd :: (c -> c) -> TripleAction a b c

LightAndLight

data Triple f a b c
  = Triple1 (f a) (f b) (f c)
  | Triple2 (f a) (f b) (f c)

data TripleAction a b c where
  Triple1Fst :: (a -> a) -> TripleAction a b c
  Triple1Snd :: (b -> b) -> TripleAction a b c
  Triple1Thd :: (c -> c) -> TripleAction a b c

LightAndLight

data Triple f a b c
  = Triple1 (f a) (f b) (f c)
  | Triple2 (f a) (f b) (f c)

data TripleAction a b c where
  Triple1Fst :: (a -> a) -> TripleAction a b c
  Triple1Snd :: (b -> b) -> TripleAction a b c
  Triple1Thd :: (c -> c) -> TripleAction a b c

LightAndLight

module Irrel where

open import Data.Bool using (if_then_else_)
open import Data.Maybe using (Maybe; just; nothing; map; _>>=_)
open import Data.Nat using (ℕ; suc; zero)
open import Data.Product using (Σ; _,_)
open import Data.String using (String; _==_)
open import Data.Unit using (⊤)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

LightAndLight

                                        x : ∀α₀, α₁, …, αₘ. (C₀, C₁, …, Cₙ) ⇒ τ
————–—————————————————————————————–————————————————————————————————————————————————————————————————————————————————–
(Θ ↓ x)  ↦  (Θ, α₀ : *, α₁ : *, …, αₘ : *, ev₀ : C₀, ev₁ : C₁, …, evₙ : Cₙ     ↑     x α₀ α₁ … αₘ ev₀ ev₁ … evₙ : τ)

—————————————————————————————————————————————————–
(Θ ↓ let x = v in e)  ↦  (Θ, [let x = ⋄ in e] ↓ v)

     solveConstraints(θ, Ξ) ↦ Ξ'       gen(Ξ', τ) ↦ σ
—————————————————————————————————————————————————————————————
(Θ, [let x = ⋄ in e], Ξ ↑ v : τ)  ↦  (θ, [let x : σ = v in ⋄] ↓ e)