Boarders

{-# language BangPatterns      #-}
{-# language OverloadedStrings #-}
module CountWords (run) where

-- pvar
import Data.Primitive.PVar

--bytestring
import Data.ByteString.Internal (ByteString(..), accursedUnutterablePerformIO)
import qualified Data.ByteString as ByteString

Boarders

module Comp where

open import Data.List
  using (List; []; _∷_; _++_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl)
open import Data.Nat
  using (ℕ; _+_)
open import Data.List.Properties
  using (++-assoc; ++-identityʳ)

Boarders

module Weird where

open import Data.List 
  using (List; []; _∷_)

data Type : Set where
  ⊤   : Type
  _⇛_ : Type → Type → Type

infix 4 _∋_

Boarders

record Peano (N : Set) (_≃_ : N -> N -> Set) : Set₁ where
  field
    zero : N
    succ : N -> N
    reflexivity : forall (a : N) -> a ≃ a
    symmetry    : forall (a b : N) -> a ≃ b -> b ≃ a
    transivity  : forall (a b c : N) -> a ≃ b -> b ≃ c -> a ≃ c
    s-injective : forall (a b : N) -> (succ a) ≃ (succ b) -> a ≃ b
    zero≠succ   : forall (a : N) -> zero ≃ (succ a) -> ⊥
    induction   : 

Boarders

{-# LANGUAGE Strict, LambdaCase, BlockArguments #-}

-- inspired by andras kovacs
module Main where

import Data.Maybe (fromJust)

main :: IO ()
main = print (nfTop True top example)

Boarders

  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100  2399  100  2399    0     0   6397      0 --:--:-- --:--:-- --:--:--  6397
downloading Nix 2.3.3 binary tarball for x86_64-darwin from 'https://nixos.org/releases/nix/nix-2.3.3/nix-2.3.3-x86_64-darwin.tar.xz' to '/var/folders/ms/pt_bh2sx27q8y_xw3gd9_5lm0000gq/T/nix-binary-tarball-unpack.XXXXXXXXXX.4CnnJMHg'...
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100 26.3M  100 26.3M    0     0  4525k      0  0:00:05  0:00:05 --:--:-- 5213k
Note: a multi-user installation is possible. See https://nixos.org/nix/manual/#sect-multi-user-installation
performing a single-user installation of Nix...
directory /nix does not exist; creating it by running 'mkdir -m 0755 /nix && chown callanmcgill /nix' using sudo

Boarders

+ set -e
+ main
+ echo ''

+ echo '     ------------------------------------------------------------------ '
     ------------------------------------------------------------------ 
+ echo '    | This installer will create a volume for the nix store and        |'
    | This installer will create a volume for the nix store and        |
+ echo '    | configure it to mount at /nix.  Follow these steps to uninstall. |'
    | configure it to mount at /nix.  Follow these steps to uninstall. |

Boarders

printResult1 : List ℕ -> IO ⊤
printResult1 ns = (putStrLn (showNat (total-fuel ns)))

printResult2 : List ℕ -> IO ⊤
printResult2 ns = (putStrLn (showNat (total-fuel-iter ns)))

printResults : List ℕ -> IO ⊤
printResults ns = printResult1 ns >> printResult2 ns

Boarders

data List (A : Set) : Set where
  [] : List A
  ∷ : A -> List A -> List A
{-# COMPILE GHC List = data List ([] | (:)) #-}

postulate
  printNats : List ℕ -> String
  ex : List ℕ
{-# COMPILE GHC printNats = printNats #-}
{-# COMPILE GHC ex        = test       #-}

Boarders

#lang scheme

;; church encoded zero
(define c-zero
  (lambda (f x) x))

;; church encoded one
(define (add-1 cn)
  (lambda (f x) (f (cn f x))))