ekmett

{-# language TypeInType, QuantifiedConstraints, ConstraintKinds, RankNTypes, UndecidableInstances, MultiParamTypeClasses, TypeFamilies, KindSignatures #-}

module QC where

import Data.Constraint
import Data.Functor.Contravariant
import Data.Kind
import Data.Profunctor

type C = (Type -> Type) -> (Type -> Type -> Type) -> Constraint

jozefg

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternGuards #-}
module Unification where
import           Control.Monad
import           Control.Monad.Gen
import           Control.Monad.Trans
import qualified Data.Map.Strict     as M
import           Data.Foldable
import           Data.Monoid

lexi-lambda

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Language.HigherRank.Main
  ( Expr(..)
  , EVar(..)
  , Type(..)
  , TVar(..)
  , TEVar(..)
  , runInfer
  ) where

treeowl

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs,
      ScopedTypeVariables, TypeOperators #-}

-- | Type-level natural numbers and singletons, with proofs of
-- a few basic properties.

module BasicNat (
    -- | Type-level natural numbers
    Nat (..)
  , type (+)

twanvl

module Sorting where
-- See https://www.twanvl.nl/blog/agda/sorting

open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List hiding (merge)
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties hiding (_≟_;_≤?_;≤-refl;≤-trans)
open import Data.Nat.Logarithm
open import Data.Nat.Induction