alecjacobson

#!/bin/bash

if [ -z "$1" ];then
  echo "USAGE:

procrusteanarxiv path/to/input/dir/containing/tex/files/

This script tested with dependencies:

gs           Ghostscript version 9.27 (9.21 is buggy)

avigad

import data.fintype tactic.ring

structure graph :=
(vertex : Type*)
(edge   : vertex → vertex → bool)

namespace graph

class undirected (G : graph) :=
(symm : ∀ x y : G.vertex, G.edge x y = G.edge y x)

mattdesl

const {
  canvasSketch,
  GUI,
  KeyPress,
  FaviconRenderer
} = require('./hooks');

const settings = {
  animate: true,
  scaleToView: true,

fpvandoorn

/-
Copyright (c) 2019 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Floris van Doorn

---

Proof that a cube (in dimension n ≥ 3) cannot be cubed:
there does not exist a partition of a cube into finitely many smaller cubes (at least two)
of different sizes.

digama0

*** The goal today is to prove the following theorem:

h50::itexp.1         |- ( ph -> A e. RR )
h51::itexp.2         |- ( ph -> B e. RR )
h52::itexp.3         |- ( ph -> A <_ B )
h53::itexp.4       |- ( ph -> N e. NN )
qed::              |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )

*** Jon thinks it would be easier to do this without the "ph ->", but I think he may regret that decision later.
*** Anyway it is epsilon harder to have a context so let's just go with it.

HarryStevens

license: gpl-3.0

PatrickMassot

{
	"Type*": {
                "prefix": "Type*",
                "body": [
                  "{$1 : Type*}$0"
                ],
        "description": "Type* variable",
        },
        "Variables": {
                "prefix": "var",

PatrickMassot

import tactic.interactive
import tactic.linarith

@[derive decidable_eq]
inductive people : Type | Brown | Jones | Smith

constant only_child : people → Prop
constant salary : people → ℕ

@[derive decidable_eq]

pdewacht

#!/usr/bin/env python3
import re, sys
from heapq import heapify, heappush, heappop

class Bot:
    def __init__(self, x, y, z, r):
        self.x = x
        self.y = y
        self.z = z
        self.r = r

duhaime

license: MIT
height: 348
scrolling: no
border: yes