Lapin0t

From Stdlib Require Import Vector.
Notation vec := Vector.t.
Arguments nil {A}.
Arguments cons {A} _ {n}.

(* For some reason cons has the length argument after the head argument, which
will be cumbersome here. *)
Definition cons' {A} n (x : A) (xs : vec A n) : vec A (S n) := cons x xs.
Arguments cons' {_} _ _ _ /.

Lapin0t

Set Primitive Projections.

From Equations Require Import Equations.
Set Equations Transparent.

Record maybe (X : Type) := {
  dom : Prop ;
  val : dom -> X ;
}.
Arguments dom {X}.

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: