pnc

#!/bin/bash

set -e

CONTENTS=$(tesseract -c language_model_penalty_non_dict_word=0.8 --tessdata-dir /usr/local/share/tessdata/ "$1" stdout -l eng | xml esc)

hex=$((cat <<EOF
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
<plist version="1.0">

ahmadsalim

AndrasKovacs

{-# OPTIONS --without-K #-}

{-
Below is an example of proving *everything* about the substitution calculus of a
simple TT with Bool.

The more challenging solution:
  - If substitutions are defined as lists of terms, then if you manage to
    prove that substitutions form a category, almost certainly you're done,
    since you can only prove this is you have all relevant lemmas.

dorchard

module Category where

open import Level
open import Relation.Binary.PropositionalEquality

open Level

record Category {lobj : Level} {larr : Level} : Set (suc (lobj ⊔ larr)) where
  field obj : Set lobj
        arr : (src : obj) -> (trg : obj) -> Set larr

gelisam

{-# OPTIONS --copatterns #-}
module Main where
-- A simple cat program which echoes stdin back to stdout, but implemented using copatterns
-- instead of musical notation, as requested by Miëtek Bak (https://twitter.com/mietek/status/806314271747481600).

open import Data.Nat

open import Data.Unit
open import Data.Bool
open import Data.Char

puffnfresh

module Main where

import IO.Primitive as Prim
open import Coinduction
open import Data.Unit
open import IO

cat : IO ⊤
cat = ♯ getContents >>= (\cs → ♯ (putStr∞ cs))

puffnfresh

module Main where

import IO.Primitive as Prim
open import Data.Unit
open import IO
open import Coinduction

nonTerminatingIO : IO ⊤
nonTerminatingIO = ♯ nonTerminatingIO >> ♯ return tt

gallais

module State where

open import Data.Unit
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality

_⟶_ : {I : Set} (X Y : I → Set) → Set
X ⟶ Y = ∀ {i} → X i → Y i

AndrasKovacs

{-# language DataKinds, PolyKinds, ScopedTypeVariables, UndecidableInstances,
    FlexibleInstances, FlexibleContexts, GADTs, TypeFamilies, RankNTypes,
    LambdaCase, TypeOperators, ConstraintKinds #-}

import GHC.TypeLits
import Data.Proxy
import Data.Singletons.Prelude
import Data.Singletons.Decide
import Data.Constraint

BekaValentine

module Scratch where

postulate
  Inf  : ∀ {a} (A : Set a) → Set a
  delay : ∀ {a} {A : Set a} → A → Inf A
  force  : ∀ {a} {A : Set a} → Inf A → A

{-# BUILTIN INFINITY Inf  #-}
{-# BUILTIN SHARP    delay #-}
{-# BUILTIN FLAT     force  #-}