rampion

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall -Werror -Wextra -Wno-name-shadowing #-}

module HyperList where

import Data.Function ((&))

newtype a -&> b = Hyp {invoke :: (b -&> a) -> b}

treeowl

-- | This module defines a function that produces a complete binary tree
-- from a breadth-first list of its (internal) node labels. It is an
-- optimized version of an implementation by Will Ness that avoids
-- any "impossible" cases. See
--
-- https://stackoverflow.com/a/60561480/1477667

module Bftr (Tree (..), bft, list, deftest) where
import Data.Function (fix)
import Data.Monoid (Endo (..))

ice1000

{-# OPTIONS --cubical #-}

open import Cubical.Core.Everything
open import Cubical.Data.Maybe
open import Cubical.Data.Nat

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

data ω : Type₀ where

inflation

*** preview.el.orig	2018-06-11 14:08:50.000000000 -0400
--- preview.el	2018-06-11 15:35:38.000000000 -0400
***************
*** 180,186 ****
  	  (close preview-gs-close))
      (tiff (open preview-gs-open)
  	  (place preview-gs-place)
! 	  (close preview-gs-close)))
    "Define functions for generating images.
  These functions get called in the process of generating inline

AndrasKovacs

{-# language TemplateHaskell, ScopedTypeVariables, RankNTypes,
             TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs,
             TypeOperators, TypeApplications, AllowAmbiguousTypes,
             TypeInType, StandaloneDeriving #-}

import Data.Singletons.TH -- singletons 2.4.1
import Data.Kind

-- some standard stuff for later examples' sake

yocontra

AOE2HD - For Mac OSX

Estimated time: 10 minutes

Purchase

• Sign in and purchase the game for $19.99

Installing PortingKit

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 (+)

dysinger

;; 1. place this in ~/.emacs.d/private/intero/packages.el

;; 2. add intero, syntax-checking and auto-completion to your
;; ~/.spacemacs layer configuration & remove the haskell layer
;; if you were using that before

;; 3. make sure you have stack installed http://haskellstack.org

;; 4. fire up emacs & open up a stack project's source files

andrejbauer

sebfisch

Delimited Continuations

Delimited continuations manipulate the control flow of programs. Similar to control structures like conditionals or loops they allow to deviate from a sequential flow of control.

We use exception handling as another example for control flow manipulation and later show how to implement it using delimited continuations. Finally, we show that nondeterminism can also be expressed using delimited continuations.

Exception Handling