fizruk

-- A Pandoc filter to use Pygments for Pandoc
-- Code blocks in HTML output
-- Nickolay Kudasov 2013
-- Requires Pandoc 1.12

import Text.Pandoc.Definition
import Text.Pandoc.JSON (toJSONFilter)
import Text.Pandoc.Shared
import Data.Char(toLower)
import System.Process (readProcess)

fizruk

{-# LANGUAGE FlexibleInstances, DeriveFunctor, TypeFamilies #-}
module Main where

import Control.Comonad.Identity
import Control.Comonad.Trans.Class
import Control.Comonad.Trans.Cofree
import Control.Monad.Trans.Free
import Control.Monad (void)

import Control.Monad.State

fizruk

version: 2

jobs:
  build:
    docker:
      - image: fpco/stack-build:lts-11.0
    steps:
      - checkout

      - restore_cache:

fizruk

Require Import UniMath.Combinatorics.FiniteSets.

Definition FiniteSetProduct (X Y : FiniteSet) : FiniteSet.
Proof.
  set (X' := pr1 X).           (* the underlying type of X *)
  set (X'_isfinite := pr2 X).  (* proof that X is a finite set *)
  set (Y' := pr1 Y).           (* the underlying type of Y *)
  set (Y'_isfinite := pr2 Y).  (* proof that Y is a finite set *)

  exists (X' × Y'). (* the underlying type for the product is the product of types *)

fizruk

let NonEmpty = λ(a : Type) → { head : a, tail : List a }
let List2 = λ(a : Type) → < Nil | Cons : NonEmpty a >

let split : ∀(a : Type) → List a → List2 a
    = λ(a : Type)
    → λ(xs : List a)
    → List/fold a xs (List2 a)
        (λ(x : a) → λ(ys : List2 a) →
          merge
          { Cons = λ(cons : NonEmpty a)

fizruk

Require Export UniMath.Foundations.Propositions.

(* A simpler definition of proposition. *)
Definition isaprop' (X : UU) : UU := ∏ (x y : X), x = y.

(* Simpler definition implies standard isaprop. *)
Definition isaprop'_to_isaprop {X : UU} :
  isaprop' X → isaprop X.
Proof.
  intros f x y.

fizruk

#! /usr/bin/env nix-shell
#! nix-shell -i runghc -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [servant-server])"
-- =======================================================================
--
-- If you have have Nix installed — just run this script as an executable:
--
-- $ ./servant-token-bearer.hs
-- Starting server at http://localhost:8088
--
-- You can then check that everything works using cURL:

fizruk

#! /usr/bin/env nix-shell
#! nix-shell -i runghc -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [servant-swagger servant-swagger-ui])"
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE DeriveAnyClass    #-}
{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds         #-}
{-# LANGUAGE TypeApplications  #-}
{-# LANGUAGE TypeFamilies      #-}

fizruk

#! /usr/bin/env nix-shell
#! nix-shell -i runghc -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [servant-swagger servant-swagger-ui])"
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE ScopedTypeVariables   #-}

fizruk

resolver: lts-6.20
compiler: ghcjs-0.2.0.9006020_ghc-7.10.3
compiler-check: match-exact

packages:
  - '.'

# where to get GHCJS from (you don't need it when using Docker)
setup-info:
  ghcjs: