jcreedcmu

import * as cp from 'child_process';

type Prop = 'a' | 'b' | [Prop, Prop];

function propToStr(p: Prop): string {
  if (typeof p === 'string') return p;
  return `im(${propToStr(p[0])}, ${propToStr(p[1])})`;
}

function propToStrIleancop(p: Prop): string {

jcreedcmu

p0 1:1

2020-06-17

• Was on break last week

• Pagination for bqrs landed, need to finish up for interpreted, then can embrace the glorious future of massive red diffs at last.

jcreedcmu

const fs = require('fs');
const qs = require('querystring');
const https = require('https');

const query = {
  key: fs.readFileSync('/home/jcreed/private/maps-api2', 'utf8').replace(/\n/g, ''),
  input: "chipotle",
  inputtype: "textquery",
  fields: "formatted_address,name",
  location: "40.7831,-73.9712", // manhattan

jcreedcmu

#include <stdio.h>
#define GOOD1  99586915107664152904966939075856564224.0
#define GOOD2 298759386401549014052982412761733529600.0
#define BAD   298759406683958617704652836708984815616.0

int isGood(float x) {
  return 1.0 / (1.0 / x) == x;
}

float disc(float x) {

jcreedcmu

type Omit<T, K extends keyof T> = Pick<T, Exclude<keyof T, K>>
type Elim<T extends { t: string }, U extends string> = T extends { t: U } ? never : T;
type Choose<T extends { t: string }, U extends string> = T extends { t: U } ? T : never;
type Prog<T, U> = { k: 'src', v: T } | { k: 'ans', v: U };

interface PreMatcher<T extends { t: string }> {
  cas<S extends string, U>(tag: S, f: (x: Omit<Choose<T, S>, 't'>) => U): Matcher<Elim<T, S>, U>;
}

interface Matcher<T extends { t: string }, U> {

jcreedcmu

type Lang = 'en' | 'es';
type Intl<T> = {
  forms: { new_form: T },
  hello: T
};

type Dict<T extends string, U> = { [k in T]: U };

type LangDataIn = Dict<Lang, Intl<string>>;
type LangDataOut = Intl<Dict<Lang, string>>;

jcreedcmu

import { range, sum, uniq } from './util';

function paths(s) {
  function swap(s, n) {
    const sc = [].concat(s);
    const tmp = sc[n];
    sc[n] = sc[n + 1];
    sc[n + 1] = tmp;
    return sc;
  }

jcreedcmu

export function range(n) {
  const rv = [];
  for (let i = 0; i < n; i++)
	 rv.push(i);
  return rv;
}

const r = Math.random;
type Point = {x: number, y: number};

jcreedcmu

module RelationList (A : Set)  where

-- Converse of relation
converse : (A → A → Set) → (A → A → Set)
converse R a a' = R a' a

-- A list of things (a1, a2, ... an) with relations
-- u -R-> a1 -R-> a2 -R-> ... -R-> an -R-> v
data Rist' (R : A → A → Set) (v : A) : (u : A) → Set where
  rnil : {u : A} → (r : R u v) → Rist' R v u

jcreedcmu

{-# OPTIONS --without-K #-}
open import HoTT

module b where

A : Set
A = ℕ

rev : (A → A → Set) → (A → A → Set)
rev R a a' = R a' a