ice1000

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;

ice1000

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()

ice1000

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

ice1000

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

ice1000

\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

ice1000

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')

ice1000

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).

ice1000

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

ice1000

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

ice1000

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude
open import Cubical.Data.List

private variable X : Type

rev-ind : (P : List X → Type)
  → P []
  → (∀ x xs → P xs → P (xs ∷ʳ x))