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

discipline = __ (!`SELECT discipline FROM "/test/testDb/olympics" LIMIT 1`) year = __ (!`SELECT year FROM "/test/testDb/olympics" LIMIT 1`) country = {!`SELECT DISTINCT country FROM "/test/testDb/olympics"`} (!`SELECT country FROM "/test/testDb/olympics" LIMIT 1`) type = (!`SELECT DISTINCT type FROM "/test/testDb/olympics" LIMIT 1`) !`SELECT DISTINCT type FROM "/test/testDb/olympics" OFFSET 1` gender = [!`SELECT gender FROM "/test/testDb/olympics" LIMIT 1`] !`SELECT DISTINCT gender FROM "/test/testDb/olympics"`

jonsterling

(* It is not possible in Standard ML to construct an identity type (or any other
 * indexed type), but that does not stop us from speculating. We can specify with
 * a signature equality should mean, and then use a functor to say, "If there
 * were a such thing as equality, then we could prove these things with it."
 * Likewise, we can use the same trick to define the booleans and their
 * induction principle at the type-level, and speculate what proofs we could
 * make if we indeed had the booleans and their induction principle.
 *
 * Functions may be defined by asserting their inputs and outputs as
 * propositional equalities in a signature; these "functions" do not compute,

jonsterling

// A nice little example of using transactional signal generators.
// Imagine a board of buttons with numbers on it, and a big red button with a picture of a bomb on it.
// When a button with a number is pressed, `increment` is invoked with that number. When the bomb
// button is pressed, then `reset` is invoked.
//
//This returns a signal of the running total made by incrementing by numbers and resetting by explosions.
RACDynamicSignalGenerator *increment = [[RACDynamicSignalGenerator alloc] initWithBlock:^RACSignal *(NSNumber *add) {
	return [RACSignal return:^(NSNumber *count) {
		return @(count.integerValue + add.integerValue);
	}];

jonsterling

module type TYPE = sig
  type t
end

module type EMPTY = functor (T : TYPE) -> sig
  val apply : T.t
end

type empty = (module EMPTY)