jonsterling

\documentclass{article}
\usepackage{libertine}
\usepackage[usenames,dvipsnames,svgnames,table]{xcolor}
\usepackage{amsmath, amssymb, proof, microtype, hyperref}
\usepackage{mathpartir} % for mathpar, not for proofs

\usepackage{perfectcut}
\newcommand\Parens[1]{\perfectparens{#1}}
\newcommand\Squares[1]{\perfectbrackets{#1}}

jonsterling

module experiment where

open import Agda.Primitive
open import Prelude.List
open import Prelude.Size
open import Prelude.Monoidal
open import Prelude.Monad
open import Prelude.Functor
open import Prelude.Natural
open Size using (∞)

jonsterling

id : type.
id/z : id.
id/s : id -o id.

answer : type.
yes : answer.
no : answer.

id/eq? : id -> id -> answer -> type.
id/eq/z/z : id/eq? id/z id/z yes.

jonsterling

(my-long-op-name first-argument
                 (something-else oh-boy
                                 here-we-go-again))


;; I would prefer:
(my-long-op-name
   first-argument
   (something-else
      oh-boy

jonsterling

signature THEORY =
sig
  type sort
  type term

  structure Var :
  sig
    include ORDERED
    val toString : t -> string
  end

jonsterling

Theorem foo : ⸤⊢ (n:nat) =(zero; succ(n); nat) -> =(zero; succ(n); nat)⸥ {
  fun-intro(n.fun-intro(x.x; eq⁼(nat-eq; zero-eq; succ-eq(hyp-eq(n)))); nat-eq)
} ext {
  lam(_.lam(x.x))
}.

Operator is-zero : (0).
⸤is-zero(n)⸥ ≝ ⸤natrec(n; unit; _._.void)⸥.

Theorem succ-not-zero : ⸤⊢ (n:nat) =(succ(n); zero; nat) -> void⸥ {

jonsterling

(unless (package-installed-p 'use-package)
  (package-refresh-contents)
  (package-install 'use-package))
(require 'use-package)


(defun jms-redprl-startup-hook ()
  "Get flycheck running when RedPRL starts."

  (flycheck-mode)

jonsterling

signature LCS_SORT =
sig
  structure AtomicSort : SORT

  type atomic = AtomicSort.t

  datatype t =
      VAL of atomic
    | KONT of atomic * atomic
    | CMD of atomic

jonsterling

ENOENT: no such file or directory, open '.babelrc'
Error: ENOENT: no such file or directory, open '.babelrc'
    at Error (native)
    at Object.fs.openSync (fs.js:549:18)
    at Object.fs.readFileSync (fs.js:397:15)
    at babelrc (/Users/jon/src/atom-language-redprl/node_modules/babelrc-rollup/dist/babelrc-rollup.js:14:47)
    at Object.<anonymous> (/Users/jon/src/atom-language-redprl/src/grammar-generator/rollup.config.js:22:11)
    at Module._compile (module.js:435:26)
    at Object.require.extensions..js (/Users/jon/src/atom-language-redprl/node_modules/rollup/bin/runRollup.js:54:8)
    at Module.load (module.js:356:32)

jonsterling

(* an abstract signature for instantiations of the existential quantifier *)
module type EXISTS =
sig
  (* the predicate *)
  type 'a phi

  (* the existential type *)
  type t

  (* the introduction rule *)