... that doesn't look crazy to me.
_______ _________
___ |________________________ /
__ /| |_ ___/ _ \_ __ \ __ /
package AYA; | |
import kala.collection.Seq; | |
import kala.collection.immutable.ImmutableSeq; | |
import kala.collection.immutable.ImmutableTreeSeq; | |
import kala.collection.mutable.MutableSeq; | |
import kala.control.Result; | |
import org.aya.generic.term.DTKind; | |
import org.aya.syntax.compile.CompiledAya; | |
import org.aya.syntax.compile.JitCon; |
from email.parser import HeaderParser | |
import imaplib | |
import time | |
import requests | |
from concurrent.futures import ThreadPoolExecutor, as_completed | |
imaplib._MAXLINE = 40000000 | |
ONE_TIME_LIMIT = 10 | |
mailparser = HeaderParser() |
open import Data.Bool.Base | |
open import Relation.Binary.PropositionalEquality.Core | |
open import Relation.Nullary | |
module _ (A : Set) (dec : (a b : A) → Dec (a ≡ b)) where | |
record DFA (S : Set) : Set where | |
field F : S → Bool | |
field t : A -> S -> S | |
data RE : Set where |
variable | |
A B : Set | |
postulate | |
Eq : A → A → Set | |
refl : (a : A) → Eq a a | |
rw : {x y : A} → Eq x y → (B : A → Set) → B x → B y | |
-- UIP missing but not needed | |
N : Set | |
Z : N | |
S : N → N |
open import Agda.Builtin.Equality | |
open import Agda.Builtin.Nat using (Nat; suc; zero) | |
cong : (f : Nat → Nat) → ∀ {a b} → a ≡ b → f a ≡ f b | |
cong f refl = refl | |
trans : ∀ {a b c : Nat} → a ≡ b → b ≡ c → a ≡ c | |
trans refl p = p | |
sym : ∀ {a b : Nat} → a ≡ b → b ≡ a | |
sym refl = refl |
\import Data.Bool | |
\import Data.List | |
\import Logic.Meta | |
\import Paths | |
\func CoNat => | |
\Sigma (f : Nat -> Bool) | |
(\Pi (i : _) -> f i = false -> f (suc i) = false) | |
\where { | |
\func blt (n m : Nat) : Bool |
module PSet3 where | |
record TermStructure : Set₁ where | |
field | |
Term : Set | |
module QPER (TS TS' : TermStructure) where | |
open TermStructure TS | |
open TermStructure TS' | |
renaming (Term to Term') |
Definition lemma {n m : nat} (p : n = m) : pred n = pred m := f_equal pred p. | |
Definition lemma2 {n m : nat} (p : n = m) : S n = S m := f_equal S p. | |
Definition lemma3 {n m : nat} (p : S n = S m) : lemma2 (lemma p) = p | |
:= match p with | eq_refl => eq_refl end. | |
(* Definition bruh {n} (a : nat) (p : S n = a) : Prop. | |
Proof. | |
destruct a. | |
- exact True. | |
- exact (@lemma2 n a (@lemma (S n) (S a) p) = p). |
Inductive nat: Type := | |
| S (n: nat) | |
| O. | |
Inductive even: nat -> Prop := | |
| Base: even O | |
| Ind: forall n, even n -> even (S (S n)). | |
Inductive ev: nat -> Prop := | |
| ev_Base: ev O |