Tantalus13A98B5F

datatype ty =
| TBool
| TFun (t1: ty, t2: ty)

type id = nat

datatype tm =
| ttrue
| tfalse
| tvar (n: id)

Tantalus13A98B5F

trait Literal[T, R]:
  def apply(v: T): R

trait Addition[R]:
  def apply(a: R, b: R): R

def getAst[R](using lit: Literal[Int, R], add: Addition[R]) =
  add(add(lit(1), lit(2)), add(lit(3), lit(4)))

//-------------------------------------------------------

Tantalus13A98B5F

Require Import Coq.Arith.PeanoNat.
Require Import Coq.Program.Tactics.
Require Import Coq.Program.Wf.
Require Import Lia.
Import PeanoNat.Nat.

Fixpoint lexical (a: nat) :=
  fix lexical' (b: nat) :=
    match b with
    | 0 => match a with

Tantalus13A98B5F

#!/usr/bin/env python
# coding: utf-8

# In[1]:


import requests
from bs4 import BeautifulSoup
import pandas as pd
from pathlib import Path

Tantalus13A98B5F

from IPython.core.magic import register_cell_magic
import subprocess
import argparse
import sys
import os

@register_cell_magic
def withsave(line, cell):
    parser = argparse.ArgumentParser()
    parser.add_argument('fname')

Tantalus13A98B5F

#!/usr/bin/env python3
'''Parse logs in structures with the help of a pushdown automata.

Grammar for the sample log file:

>This line is used for exact match.
$This line is used for regexp match.
 This line is ignored.
 The following lines marked a repeated region.
!repeat

Tantalus13A98B5F

#!/usr/bin/env bash
TEMPDIR=$(mktemp -d)
cat >$TEMPDIR/input.txt
FZFOPTS="$(echo "$FZF_DEFAULT_OPTS" | sed 's/--height\s*\S*\s*//')"

for arg; do
    FZFARGS="$FZFARGS \"$arg\""
done

cat >$TEMPDIR/script.sh <<EOF

Tantalus13A98B5F

from tkinter.filedialog import askdirectory
from tkinter import *
from tkinter.ttk import *
import subprocess
import weakref
import sys
import os


def human_size(cntbytes):

Tantalus13A98B5F

import subprocess as subp
import pandas as pd
from matplotlib import pyplot as plt

p = subp.Popen(['tasklist', '/fo', 'csv'], stdout=subp.PIPE)
df = pd.read_csv(p.stdout, encoding='gbk')
df['mem'] = df['内存使用 '].transform(lambda x: int(x[:-2].replace(',', '')))
df['proc'] = df['映像名称']
df = df.groupby('proc')['mem'] \
        .agg(['sum', 'count']) \

Tantalus13A98B5F

'''My Simple PDF Parser
Can inspect the size of a PDF file.
'''
from contextlib import suppress, redirect_stdout
from collections import deque, OrderedDict
from weakref import ref
import re


class PDFRef: