Saizan

{-# LANGUAGE UndecidableInstances, OverlappingInstances, MultiParamTypeClasses, FunctionalDependencies, TypeOperators
           , TypeFamilies, EmptyDataDecls, FlexibleInstances, ScopedTypeVariables, KindSignatures, GADTs #-}

module Uncurry where

data Fun :: * -> * -> * -> * where
  Done :: Fun () r r
  Moar :: Fun xs f r -> Fun (x,xs) (x -> f) r

class Uncurry args func result | func -> args, func -> result, args result -> func where

Saizan

module Rev where

open import Data.List.Reverse
open import Relation.Binary.PropositionalEquality as PE
open import Relation.Binary.HeterogeneousEquality
open import Data.List
open import Data.Empty
open import Data.Product
open import Data.List.Properties