jespercockx

{-# OPTIONS --guardedness #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.Size

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

useronym

open import Data.Nat
open import Data.Bool

mutual
  data Stream (A : Set) : Set where
    []ˢ : Stream A
    _∷ˢ_ : A → ∞Stream A → Stream A

  record ∞Stream (A : Set) : Set where
    coinductive

L-TChen

{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE TypeInType , ScopedTypeVariables , TypeFamilies, TypeOperators #-} 
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE Safe #-}

module Unification where

import Data.Kind
import Prelude hiding ((++))

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