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:

fizruk

version: 2

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

      - restore_cache:

fizruk

1. Put irunner.js into your repository at ghcjs/lib/etc/irunner.js.
2. Put static content (CSS, images, etc.) for executable at <executable name>/static.
3. Put ghcjsiClient.html to <executable name>/static and add any headers you want.
4. Run run.sh <package name> <executable name>.

Caveats

npm packages

In order for everything to work you need to install a few packages via npm.

fizruk

class AllReflectMethod methods where
  reflectMethods :: Proxy methods -> [Method]

instance AllReflectMethod '[] where
  reflectMethods _ = []

instance (ReflectMethod m, AllReflectMethod ms) => AllReflectMethod (m:ms) where
  reflectMethods _ = reflectMethod (Proxy @m) : reflectMethods (Proxy @ms)

instance OVERLAPPING_