aljce

struct Group<'a> {
    name: &'a str,
    groups: Vec<&'a str>
}

fn is_whitespace(c: char) -> bool {
    c == ' ' || c == '\t' || c == '\n'
}

fn isnt_whitespace(c: char) -> bool {

aljce

{-# LANGUAGE MultiParamTypeClasses, 
             FunctionalDependencies,
             FlexibleInstances #-} --Three extensions compared to just type families
{-# LANGUAGE TypeFamilies #-}
module Mtl where
newtype ReaderT r m a = ReaderT { unReaderT :: r -> m a }

instance (Functor m) => Functor (ReaderT r m) where
  fmap f (ReaderT x) = ReaderT (\k -> fmap f (x k))

aljce

let
  pkgs = import <nixpkgs> {};
  stdenv = pkgs.stdenv;
  top-level = import ./top-level.nix { haskellPackages = pkgs.haskellPackages;
                                       dontCheck = pkgs.haskell.lib.dontCheck;
                                       testTopLevel = false; };
in {
  haskellEnv = stdenv.mkDerivation {
    name = "haskell-env";
    version = "1.1.1.1";

aljce

let pkgs = import <nixpkgs> { };
    top-level = import ./top-level.nix { haskellPackages = pkgs.haskellPackages;
                                         dontCheck = pkgs.haskell.lib.dontCheck;
                                         cabal-install = pkgs.cabal-install;
                                         testTopLevel = false; };
in
{ haskell-env = pkgs.stdenv.mkDerivation {
    name = "haskell-env";
    buildInputs = [ pkgs.cabal-install top-level.frank.env ];
  };

aljce

module Id where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

sym : ∀ {A} {x y : A} -> x ≡ y -> y ≡ x
sym refl = refl

_qed : ∀ {A} -> (x : A) -> x ≡ x
_ qed = refl

aljce

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
module Simple where

import Data.Kind (Type)

aljce

module Monad where

open import Data.Nat
open import Data.Vec hiding (_>>=_)

record Monad (m : Set -> Set) : Set₁ where
  infixl 1 _>>=_
  field
    pure : ∀ {a : Set} -> a -> m a
    _>>=_ : ∀ {a b : Set} -> m a -> (a -> m b) -> m b

aljce

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}
module Unsafe.Maybe where

import GHC.Prim (Addr#,nullAddr#,addrToAny#,anyToAddr#,eqAddr#,unsafeCoerce#)
import GHC.Magic (runRW#)
import GHC.Types (Any)
import Unsafe.Coerce (unsafeCoerce)

aljce

module Chapter2 where

open import Agda.Builtin.FromNat
open import Data.Nat using (ℕ; zero; suc)
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.Core using (Decidable)
open import Relation.Binary.PropositionalEquality

aljce

module Co where

open import Level hiding (suc)
open import Size
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Nat hiding (_⊔_)
open import Data.Vec using (Vec ; [] ; _∷_)
open import Data.List using (List ; [] ; _∷_)