copumpkin

module Prime where

open import Coinduction

open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Divisibility
open import Data.Fin hiding (pred; _+_; _<_; _≤_; compare)
open import Data.Fin.Props hiding (_≟_)

andrejbauer

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

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

yocontra

AOE2HD - For Mac OSX

Estimated time: 10 minutes

Purchase

• Sign in and purchase the game for $19.99

Installing PortingKit

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

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

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

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