gallais

{-# OPTIONS --copatterns #-}

module UntypedLambda where

open import Size
open import Function

mutual

  data Delay (A : Set) (i : Size) : Set where

gallais

module Rot13 where

import Control.Monad (guard)
import Data.Char (ord, chr, toLower, isLower)
import Data.Function (on)
import Data.List (sortBy)
import Data.Maybe (mapMaybe)

import Data.Set (Set)
import qualified Data.Set as Set

gallais

module Container

%default total

record Container where
  constructor MkContainer
  shape : Type
  position : shape -> Type

container : Container -> Type -> Type

gallais

{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE PolyKinds                 #-}

module ImperativeDSL where

gallais

import Data.Maybe
import Control.Monad
import Control.Applicative
import Graphics.Gloss
import Graphics.Gloss.Interface.Pure.Game

type Coordinates = (Int, Int)

data Player = Nought | Cross

gallais

{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE RankNTypes          #-}

module MutuallyDefined where

import Data.Type.Natural

gallais

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE PolyKinds            #-}

module STLC where

-- Defining type and the corresponding singletons

gallais

module Error

export
data Error : (err, a : Type) -> Type where
  MkError : (forall r. (err -> r) -> (a -> r) -> r) -> Error err a

export %inline
runError : Error err a -> (err -> r) -> (a -> r) -> r
runError (MkError hdl) kE kV = hdl kE kV

gallais

module LambdaLetRec

import Data.List1
import Data.List.Quantifiers

--------------------------------------------------------------------------------
-- types

infixr 5 ~>

gallais

import Data.String
import Data.List
import Data.List.Elem
import Decidable.Decidable
import Decidable.Equality

%default total

toWitness : (prf1 : Dec a) -> IsYes prf1 -> a
toWitness (Yes prf2) x = prf2