Molly Stewart-Gallus mstewartgallus

## syntactic.v
Require Import Coq.Unicode.Utf8.
Require Import Coq.Program.Equality.

Inductive U :=
| const (A: Type)

| id
(* | compose (τ0 τ1: U) *)

| empty

## fixed.v
Set Primitive Projections.

Require Import Coq.Unicode.Utf8.

Reserved Infix "∈" (at level 90, right associativity).

Variant fiber {A B} (f: A → B): B → Type :=
  | fiber_intro x: fiber f (f x).
Arguments fiber_intro {A B f}.

## kappa.v
Require Import Coq.Unicode.Utf8.
Require Import Coq.Program.Equality.
Require Import Coq.Logic.FunctionalExtensionality.
Require Coq.Lists.List.

Import List.ListNotations.

Reserved Notation "Γ ⊢ Δ ⇒ τ" (at level 90).
Reserved Notation "x ∈ Γ" (at level 90).
Reserved Infix "$" (at level 20, left associativity).

## zippertypetheory.v
Global Set Primitive Projections.

Require Import Coq.Unicode.Utf8.
Require Coq.Lists.List.

Import List.ListNotations.

Variant zipper {A} := zip (Γ1: list A) (τ: A) (Γ2: list A).
Arguments zipper: clear implicits.

## silliness.jsx
import {
    lazy, Suspense,
    createContext, useCallback, useContext, useEffect, useReducer, useTransition
} from "react";

const initialState = {
    poison: false,
    throwable: undefined
};

## panel.jsx
import { useId, useState, useCallback } from "react";

const Panel = ({children, heading}) => {
    const detailsId = useId();
    const headingTextId = useId();
    const headingId = useId();
    const contentId = useId();
    const [open, setOpen] = useState(false);

    const onToggle = useCallback(e => {

## impredicative_induction.v
Require Import Coq.Unicode.Utf8.

(* ana is short for anafunction, not really a better name *)
Definition ana A := { P: A → Prop | exists! a: A, P a }.

Definition map {A B} (f: A → B) (x: ana A): ana B.
Proof.
  exists (λ b, ∃ a, proj1_sig x a ∧ f a = b).
  destruct x as [? [a p]].
  exists (f a).

## sandbox.jsx
import * as React from "react";

const empty = `<!DOCTYPE>
<html>
<body>
</body>
</html>
`;

export const Sandbox = ({children}) => {

## ceskusecase.js
class Control {
    to(name, rest) {
        return new LetControl(name, this, rest);
    }

    apply(x) {
        return new ApplyControl(this, x);
    }

    map(f) {

## weirdness.js
document.location.replace(URL.createObjectURL(new Blob([`<!DOCTYPE html>
<html>
<head>
<title>Lol</title>
<script>
history.replaceState(null, null, "lol");
</script>
</head>
<body>
lol lmao
	Require Import Coq.Unicode.Utf8.
	Require Import Coq.Program.Equality.

	Inductive U :=
	\| const (A: Type)

	\| id
	(* \| compose (τ0 τ1: U) *)

	\| empty
	Set Primitive Projections.

	Require Import Coq.Unicode.Utf8.

	Reserved Infix "∈" (at level 90, right associativity).

	Variant fiber {A B} (f: A → B): B → Type :=
	\| fiber_intro x: fiber f (f x).
	Arguments fiber_intro {A B f}.
	Require Import Coq.Unicode.Utf8.
	Require Import Coq.Program.Equality.
	Require Import Coq.Logic.FunctionalExtensionality.
	Require Coq.Lists.List.

	Import List.ListNotations.

	Reserved Notation "Γ ⊢ Δ ⇒ τ" (at level 90).
	Reserved Notation "x ∈ Γ" (at level 90).
	Reserved Infix "$" (at level 20, left associativity).
	Global Set Primitive Projections.

	Require Import Coq.Unicode.Utf8.
	Require Coq.Lists.List.

	Import List.ListNotations.

	Variant zipper {A} := zip (Γ1: list A) (τ: A) (Γ2: list A).
	Arguments zipper: clear implicits.
	import {
	lazy, Suspense,
	createContext, useCallback, useContext, useEffect, useReducer, useTransition
	} from "react";

	const initialState = {
	poison: false,
	throwable: undefined
	};
	import { useId, useState, useCallback } from "react";

	const Panel = ({children, heading}) => {
	const detailsId = useId();
	const headingTextId = useId();
	const headingId = useId();
	const contentId = useId();
	const [open, setOpen] = useState(false);

	const onToggle = useCallback(e => {
	Require Import Coq.Unicode.Utf8.

	(* ana is short for anafunction, not really a better name *)
	Definition ana A := { P: A → Prop \| exists! a: A, P a }.

	Definition map {A B} (f: A → B) (x: ana A): ana B.
	Proof.
	exists (λ b, ∃ a, proj1_sig x a ∧ f a = b).
	destruct x as [? [a p]].
	exists (f a).
	import * as React from "react";

	const empty = `<!DOCTYPE>
	<html>
	<body>
	</body>
	</html>
	`;

	export const Sandbox = ({children}) => {
	class Control {
	to(name, rest) {
	return new LetControl(name, this, rest);
	}

	apply(x) {
	return new ApplyControl(this, x);
	}

	map(f) {
	document.location.replace(URL.createObjectURL(new Blob([`<!DOCTYPE html>
	<html>
	<head>
	<title>Lol</title>
	<script>
	history.replaceState(null, null, "lol");
	</script>
	</head>
	<body>
	lol lmao