LightAndLight

{-# language GADTs #-}
{-# language RankNTypes #-}\
{-# options_ghc -Wall -Werror #-}
module Path where

data Expr
  = Add Expr Expr
  | Int Int
  | Declare String Expr

LightAndLight

Pi : (A:Type) -> (A -> Type) -> Type
Pi s t = (x:s) -> t x

Sigma : (A:Type) -> (A -> Type) -> Type
Sigma s t = (x:s ** t x)

uncurry :
  {A:Type} ->
  {B:A->Type} ->
  {C:(x:A)->B x->Type} ->

LightAndLight

{-# language GADTs, KindSignatures, DataKinds #-}
{-# language TemplateHaskell #-}

import Data.Kind (Type)
import Data.Ratio (Rational)
-- dependent-map
import Data.Dependent.Map (DMap)
import qualified Data.Dependent.Map as DMap
-- dependent-sum-template
import Data.GADT.Compare.TH (deriveGEq, deriveGCompare)

LightAndLight

module Codec

%default total

data Bits : Nat -> Type where
  Nil : Bits 0
  Snoc : 
    {n:Nat} -> 
    Bits n -> 
    Bool -> 

LightAndLight

module Main where 

data Thin a = Thin [Int] a

data Exp
  = Var
  | Lam Bool (Thin Exp)
  | App (Thin Exp) (Thin Exp)

data Closure a = Closure (Scope a) a

LightAndLight

--- begin some_template.string ---
Hello, this a big long string. It's an expression.
It might reference variables, like this: $ref1, or this: ${ref2.property}
---  end  some_template.string ---

--- begin three.expr ---
1 + 2

LightAndLight

{-# language GADTs, StandaloneDeriving #-}
{-# language LambdaCase #-}
{-# language MultiParamTypeClasses #-}
{-# language TemplateHaskell #-}
module Graph where

import Control.Applicative
import Data.Dependent.Map (DMap)
import Data.Dependent.Sum (ShowTag(..))
import Data.GADT.Compare.TH (deriveGEq, deriveGCompare)

LightAndLight

module Red where

open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; Extensionality; sym)
open import Data.Fin using (Fin; suc; zero)
open import Data.Nat using (ℕ; suc; zero)
open import Data.Vec using (Vec; _∷_; []; lookup; _[_]=_; here; there)
open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)

LightAndLight

module Load where

import Distribution.ModuleName (ModuleName)
import Distribution.PackageDescription.Parsec (readGenericPackageDescription)
import Distribution.Simple (simpleUserHooks)
import Distribution.Simple.BuildPaths (getLibSourceFiles)
import Distribution.Simple.Configure (findDistPrefOrDefault, configure)
import Distribution.Simple.Flag (fromFlagOrDefault, flagToMaybe, toFlag)
import Distribution.Simple.LocalBuildInfo (localPkgDescr, withLibLBI)
import Distribution.Simple.Program.Db (defaultProgramDb)

LightAndLight

YOUR SHOT