no crypto

src/Crypto/RSA.agda

@@ -1,36 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module Crypto.RSA where
-
-open import Agda.Builtin.Cubical.Path
-open import Crypto.RSA.Nat
-
-refl : {A : Set} {x y : A} → x ≡ y
-refl {A} {x} {y} i = x
-
-data Σ (A : Set) (B : A → Set) : Set where
-  ⟨_,_⟩ : (x : A) → B x → Σ A B
-
-∃ : ∀ {A : Set} (B : A → Set) → Set
-∃ {A} B = Σ A B
-
-∃-syntax = ∃
-syntax ∃-syntax (λ x → B) = ∃[ x ] B
-
-record divides (d n : ℕ) : Set where
-  constructor mkDivides
-  field
-    p : ∃[ m ] (d * m ≡ n)
-
--- doesDivide : (d n : ℕ) → Dec (divides d n)
--- doesDivide zero n = yes refl
--- doesDivide (suc d) n = ?
-
-record prime (n : ℕ) : Set where
-  constructor mkPrime
-  field
-    p : ∀ (x y : ℕ) → ¬ (x * y ≡ n)
-
-isPrime : (n : ℕ) → Dec (prime n)
-isPrime zero = ?
-isPrime (suc n) = ?

src/Crypto/RSA/Nat.agda

@@ -1,39 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module Crypto.RSA.Nat where
-
-open import Agda.Builtin.Cubical.Path
-
-infixl 6 _+_
-infixl 7 _*_
-
-data Bool : Set where
-  true : Bool
-  false : Bool
-
-record ⊥ : Set where
-
-¬_ : Set → Set
-¬ x = ⊥
-
-data Dec (A : Set) : Set where
-  yes : A → Dec A
-  no : ¬ A → Dec A
-
-data ℕ : Set where
-  zero : ℕ
-  suc : ℕ → ℕ
-
-{-# BUILTIN NATURAL ℕ #-}
-
-data Fin : ℕ → Set where
-  zero : {n : ℕ} → Fin (suc n)
-  suc : {n : ℕ} → (i : Fin n) → Fin (suc n)
-
-_+_ : ℕ → ℕ → ℕ
-zero + y = y
-suc x + y = suc (x + y)
-
-_*_ : ℕ → ℕ → ℕ
-zero * y = zero
-suc x * y = y + x * y