maxsnew

module Foo where

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

record NamedPair (A B : Set) : Set where
  pattern -- not allowed to pattern match on NamedPair otherwise
  no-eta-equality
  field
    fst : A

maxsnew

{-# OPTIONS --safe #-}
module Cubical.Foundations.Isomorphism.More where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Sigma

private
  variable

maxsnew

{-# OPTIONS --guarded #-}
module GuardedKanren where

open import Agda.Primitive using (Level; _⊔_)
private variable
  l l' : Level
  A B : Set l

data Bool : Set where true false : Bool
if_then_else_ : ∀{A : Set} → Bool → A → A → A

maxsnew

module ChurchList where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
import Cubical.Data.List as List
open import Cubical.Data.List using (List)

private
  variable ℓ : Level

maxsnew

Require Import Coq.Bool.Bool.

Inductive Sexp :=
| Atom : bool -> Sexp
| List : Forest -> Sexp
with
Forest :=
| Nil : Forest
| Cons : Sexp -> Forest -> Forest.

maxsnew

#lang typed/racket

(define-type Var String)
(define-type Type (U 'Base (List '-> Type Type)))
(define-type Ctx  (Listof (Pair Var Type)))
(define-type Expr (U Var (List 'App Expr Term) (List 'Asc Type Term)))

(define-type Lam (List 'Lam Var Term))
(define-type Term (U Expr Lam))
(define-predicate lam? Lam)

maxsnew

def print_upper(s : str):
    up_s = s.upper()
    def printer(n : int):
        acc = ""
        for i in range(0,n):
            acc += up_s
        return acc
    return printer

maxsnew

[mnew:~CODE/racket/Redex-Enum-Paper]$ scribble --latex --dest x paper.scrbl                                                                                                                              (master) 
 [Output to x/paper.tex]
Warning: some cross references may be broken due to undefined tags:
 (counter ("figure" "fig:benchmark-lines"))
 (counter ("figure" "fig:benchmark-lines" "value"))
 (counter ("figure" "fig:benchmark-overview"))
 (counter ("figure" "fig:benchmark"))
 (counter ("figure" "fig:correlation" "value"))
 (counter ("figure" "fig:benchmark-overview" "value"))
 (counter ("figure" "fig:benchmark" "value"))

maxsnew

extern crate graphviz;

use graphviz as dot;
use std::str;

type Nd = uint;
type Ed = (uint, uint);
struct Graph<'a> {
    nodes: Vec<&'a str>,
    edges: Vec<Ed>,

maxsnew

data Request = PutS String
             | Exit Int
             | GetS

port out : Signal (Maybe Request)