Lapin0t

-- Source: Conor McBride
-- https://personal.cis.strath.ac.uk/conor.mcbride/fooling/Jigger.agda
module Jigger where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero + n = n

Lapin0t

module test where

data ty : Set where
  unit : ty
  _⇒_ : ty → ty → ty

data env : Set where
  ∅ : env
  _▸_ : env → ty → env

Lapin0t

module tele where

open import Function.Bundles
open import Level hiding (lift; zero; suc)
open import Data.Product
open import Data.Product.Properties using (Σ-≡,≡↔≡)
open import Data.Unit
open import Data.Nat hiding (_⊔_)
open import Data.Fin hiding (lift)

Lapin0t

// ==UserScript==
// @name        New script - youtube.com
// @namespace   Violentmonkey Scripts
// @match       https://www.youtube.com/
// @grant       GM_notification
// @grant       GM_xmlhttpRequest
// @grant       GM_getValue
// @grant       GM_setValue
// @version     1.0
// @author      -

Lapin0t

module simple where

open import Agda.Builtin.Size public

_∘_ : ∀ {i j k} {A : Set i} {B : A → Set j} {C : ∀ {x} → B x → Set k}
      (f : ∀ {x} (y : B x) → C y) (g : (x : A) → B x) (x : A) → C (g x)
f ∘ g = λ x → f (g x)

data _≡_ {i} {X : Set i} (x : X) : {Y : Set i} → Y → Set where
  refl : x ≡ x

Lapin0t

related ideas:

- the code should only query a config which would has been populated by
  command-line args or by some config file
- sync the config and the CLI so that everything can be set from CLI or in
  config file with somewhat the same names

---

$ whipper --help

Lapin0t

(lambda r,e:e(r(r('(λip·(λr,e,it,t,f·e((λc·e(print(sum(1 for(a,b)in c if x+y>a '
'and a+b>x))for(x,y)in(f()for _ in r(m))))([t(f())[2:]for _ in r(n)])for(n,m)in'
' it.takewhile(λx·x!=(0,0),(t(f())for _ in it.repeat(None)))))(range,λi·ip("fun'
'ctools").reduce(λx,y·None,i),ip("itertools"),tuple,λ·map(int,input().split()))'
')(__import__)','λ','lambda '),'·',':')))(str.replace,eval)

Lapin0t

Keybase proof

I hereby claim:

• I am lapin0t on github.
• I am lapinot (https://keybase.io/lapinot) on keybase.
• I have a public key ASBhhz1PHZ0acYsVcWteheVp7jFraGZafgc3dgsz0t2uOwo

To claim this, I am signing this object:

Lapin0t

from math import ceil as ceil_, floor as floor_, log
from matplotlib import pyplot as plt
import numpy as np

ceil = lambda n: int(ceil_(n))
floor = lambda n: int(floor_(n))

immeuble = lambda i: lambda j: j >= i

def etage_fatal(k, n, fatal):

Lapin0t

(lambda x: lambda y: y)(__import__('sys').setrecursionlimit(2**31-1))((lambda
z: (lambda s: (lambda h: (lambda j: (lambda o: (lambda d: (lambda t: (lambda
e: (lambda g: (lambda k: (lambda l: (lambda m: (lambda n: (lambda q: (lambda
r: (lambda l: (lambda v: (lambda a: (lambda p: print(a(e(p)), a(g(p)))))(lambda
x: e(x)(lambda x: x+1)(g(x)(lambda x: x-1)(0)))(v(lambda x: lambda y: (lambda
w: v(lambda p: lambda a: v((lambda u: u(u))(lambda u: (lambda f: lambda i:
lambda e: lambda g: (q(w)(i))(lambda x: j)(h)(lambda _: k(e)(g))(lambda _: v(
lambda j: lambda k: (lambda a: lambda b: lambda c: (o(d(r(a))(t(d(r(b))(r(c))
)))(t(o(r(a))(o(r(b))(r(c))))))(lambda _: f(s(i))(j)(k))(lambda _: f(s(i))(e)
(g)))(m(n(m(p)(x))(m(k)(y)))(n(m(a)(y))(m(j)(x))))(m(n(m(e)(x))(m(k)(y)))(n(m