joelburget

[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL)
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s_2 () Bool false)

joelburget

{ pkgs, ... }:

{
  home.packages = with pkgs; with pkgs.ocamlPackages; with pkgs.coqPackages; [
    anki
    htop
    # 1password
    atom
    bash
    binutils

joelburget

examples/accounts/accounts.pact:177:2:Warning: Unexpected node in translation: App {_aNode = enforce-one33::bool, _aAppFun = FNative {_fInfo = , _fName = "enforce-one", _fTypes = (msg:string tests:[bool] -> bool) :| [], _fSpecial = Nothing}, _aAppArgs = [Prim {_aNode = string34::string, _aPrimValue = PrimLit "Cancel can only be effected by creditor, or debitor after timeout"},List {_aNode = list35::[bool], _aList = [App {_aNode = enforce-keyset36::bool, _aAppFun = FNative {_fInfo = , _fName = "enforce-keyset", _fTypes = (keyset-or-name:<k[string,keyset]> -> bool) :| [], _fSpecial = Nothing}, _aAppArgs = [Var {_aNode = let4_ck15::keyset}]},App {_aNode = and37::bool, _aAppFun = FNative {_fInfo = , _fName = "and", _fTypes = (x:bool y:bool -> bool) :| [], _fSpecial = Nothing}, _aAppArgs = [App {_aNode = enforce38::bool, _aAppFun = FNative {_fInfo = , _fName = "enforce", _fTypes = (test:bool msg:string -> bool) :| [], _fSpecial = Nothing}, _aAppArgs = [App {_aNode = >=39::bool, _aAppFun = FNative {_fInfo = , _fNam

joelburget

{-# language DataKinds                  #-}
{-# language FlexibleContexts           #-}
{-# language FlexibleInstances          #-}
{-# language GADTs                      #-}
{-# language LambdaCase                 #-}
{-# language PatternSynonyms            #-}
{-# language PolyKinds                  #-}
{-# language TypeApplications           #-}
{-# language TypeOperators              #-}

joelburget

import Data.Vinyl
-- import Data.Vinyl.Functor

type LifeForm a =
    "name"     ::: String
  : "age"      ::: Int
  : "sleeping" ::: Bool
  : a

type LifeForm' a = FieldRec (LifeForm a)

joelburget

{-# language LambdaCase #-}
{-# language PatternSynonyms #-}
{-# language ViewPatterns #-}
{-# language DeriveFunctor #-}
{-# language DeriveFoldable #-}
{-# language DeriveTraversable #-}
{-# language TypeSynonymInstances #-}
{-# language FlexibleContexts #-}
{-# language FlexibleInstances #-}
module Main where

joelburget

import           Control.Monad.Trans.Reader

data Expr a
    = Var Int
    | App (Expr a) (Expr a)
    | Lam (Expr a)
    | Lit a
    | Let String (Expr a) (Expr a)
    deriving (Show)

joelburget

module Plur = struct
  type 'a t =
  | Zero
  | One of 'a
  | Two of 'a * 'a

  let return x = One x

  let (++) r1 r2 = match r1, r2 with
    | _, Zero -> r1

joelburget

{-# language LambdaCase #-}
module Data.Plur (Plur(..), count) where

import Data.Monoid

-- Plurality monad: Zero, one, or at least two.
data Plur a
  = Zero
  | One a
  | Two a a

joelburget

(enforce-pact-version "2.3")

(define-keyset 'central-bank-admin-keyset
  (read-keyset "central-bank-admin-keyset"))

(module central-bank-module 'central-bank-admin-keyset
  "central bank"

  (defschema central-bank-schema
    ("central bank"