pnlph

module test where


open import Data.Nat
open import Data.Product

foo : ℕ → ℕ
foo = λ where
  zero → 1
  (suc x) → 0

pnlph

module 4648̣ where

open import Agda.Builtin.List using (List ; _∷_)

a∷as:ListA : ∀ {A : Set} → ∀ {a : A} → ∀ {as : List A} → List A
a∷as:ListA {X} {x} {xs} = x ∷ xs

variable
  I : Set

pnlph

module issue.#3135 where

-- latex \sqw
postulate
  A : Set
  □   : Set
  _□  : Set → Set
  ⟨_⟩ : Set → Set

--G : Set

pnlph

module compilers where

module 1960s where
  open import Agda.Builtin.Nat using (_+_ ; _*_)
  open import Agda.Builtin.Equality using (_≡_ ; refl)
  _ : 5 + 6 ≡ 11
  _ = refl

module 1950s where
  open import Agda.Builtin.Nat using (Nat)

pnlph

\prec Precedes. Unicode U+227A: ≺
\preceq Precedes or equals to. Unicode U+227C: ≼
\precsim Precedes or equivalent to. Unicode U+227E: ≾
\precnsim Precedes and not equivalent to. Unicode U+22E8: ⋨

pnlph

{-#  OPTIONS --type-in-type #-}
{- 
  Computer Aided Formal Reasoning (G53CFR, G54CFR)
  Thorsten Altenkirch

  Lecture 20: Russell's paradox

  In this lecture we show that it is inconsistent to have
  Set:Set. Luckily, Agda is aware of this and indeed 
  Set=Set₀ : Set₁ : Set₂ : ...

pnlph

module sort where

-- Polymorphic types
-- Not the framework of pure type systems!
-- Reference https://jesper.sikanda.be/posts/agdas-new-sorts.html

------------------------------------------------------------
-- id₁ : id-sort₁ : Setω
-- with Level, Setω
------------------------------------------------------------

pnlph

_≤_ _≥_ : ℕ → ℕ → 𝓤₀ ̇
0      ≤ y      = 𝟙
succ x ≤ 0      = 𝟘
succ x ≤ succ y = x ≤ y

_≤'_ : ℕ → ℕ → 𝓤₀ ̇
_≤'_ = ℕ-iteration (ℕ → 𝓤₀ ̇ ) (λ y → 𝟙) (λ f → ℕ-recursion (𝓤₀ ̇ ) 𝟘 (λ y P → f y))

x ≥ y = y ≤ x

pnlph

ℕ-induction : (A : ℕ → 𝓤 ̇ ) → A 0 → ((n : ℕ) → A n → A (succ n)) → (n : ℕ) → A n
ℕ-induction A a₀ f = h where h : (n : ℕ) → A n
  h 0        = a₀
  h (succ n) = f n (h n)

ℕ-recursion : (X : 𝓤 ̇ ) → X → (ℕ → X → X) → ℕ → X
ℕ-recursion X = ℕ-induction (λ _ → X)

ℕ-iteration : (X : 𝓤 ̇ ) → X → (X → X) → ℕ → X
ℕ-iteration X x f = ℕ-recursion X x (λ _ x → f x)

pnlph

module reflection-issue where

open import Data.Nat using (zero)
open import Data.Vec using (_∷_)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Reflection using (con)
open import Data.List using ([])

_ : quoteTerm zero ≡ con (quote zero) []
_ = refl