text:
module Misc.NumeralSystem where -- One Numeral System to rule them all!?

open import Data.Maybe using (Maybe; nothing; just)
open import Data.Nat
open import Data.Product

open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Nullary using (¬_ ; yes; no)

open import Relation.Binary

open import Level
  renaming (zero to lzero; suc to lsuc)

open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; setoid; cong)

open import Data.Nat.Properties using (≤-step)
open DecTotalOrder Data.Nat.decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)

infixr 5 _∷[_,_]_

--------------------------------------------------------------------------------
--  PN - Positional Notation
--  http://en.wikipedia.org/wiki/Positional_notation
--
--  base: b
--  digits: consecutive ℕ from m to n
--                             ●────○

data PN (b m n : ℕ) : Set where
  [_] : m < n → PN b m n
  _∷[_,_]_ : (x : ℕ) → (m ≤ x) → (x < n) → PN b m n → PN b m n

--------------------------------------------------------------------------------
toℕ : ∀ {b m n} → PN b m n → ℕ
toℕ [ _ ] = 0
toℕ {b} (x ∷[ x≥m , x<n ] xs) = x + b * toℕ xs

private
   ≤→< : ∀ {m n} → m ≤ n → ¬ (m ≡ n) → m < n
   ≤→< {n = zero} z≤n 0≠0 = ⊥-elim (0≠0 refl)
   ≤→< {n = suc n} z≤n neq = s≤s z≤n
   ≤→< (s≤s m≤n) 1+m≠1+n = s≤s (≤→< m≤n (λ m≡n → 1+m≠1+n (cong suc m≡n)))

--------------------------------------------------------------------------------
-- increment
-- the image of 'incr' is "continuous" if when
--    b = 1 ⇒ m ≥ 1, n ≥ 2m
--    b > 1 ⇒ m ≥ 0, n ≥ m + b, n ≥ 1 + mb

incr : ∀ {b m n} → m ≤ 1 → 2 ≤ n → PN b m n → PN b m n
incr m≤1 2≤n [ m<n ] = 1 ∷[ m≤1 , 2≤n ] [ m<n ]
incr {b} {m} {n} m≤1 2≤n (x ∷[ m≤x , x<n ] xs) with suc x ≟ n
incr {b} {m} m≤1 2≤n (x ∷[ m≤x , x<n ] xs) | no  1+x≠n = suc x ∷[ ≤-step m≤x , ≤→< x<n 1+x≠n ] xs
incr {b} {m} m≤1 2≤n (x ∷[ m≤x , x<n ] xs) | yes refl  = m ∷[ ≤-refl , s≤s m≤x ] incr m≤1 2≤n xs

base=1-incr : ∀ {m n} → 1 ≤ m → m * 2 ≤ n → PN 1 m n → PN 1 m n
base=1-incr {m} {n} 1≤m 2m≤n [ m<n ] = m ∷[ ≤-refl , m<n ] [ m<n ]
base=1-incr {m} {n} 1≤m 2m≤n (x ∷[ m≤x , x<n ] xs) with suc x ≟ n
base=1-incr {m} {n} 1≤m 2m≤n (x ∷[ m≤x , x<n ] xs) | no 1+x≠n = suc x ∷[ ≤-step m≤x , ≤→< x<n 1+x≠n ] xs
base=1-incr {m} 1≤m 2m≤n (x ∷[ m≤x , x<n ] xs) | yes refl = m ∷[ ≤-refl , s≤s m≤x ] base=1-incr 1≤m 2m≤n xs

base>1-incr : ∀ {b m n} → 1 < b → 0 ≤ m → m + b ≤ n → m * b + 1 ≤ n → PN b m n → PN b m n
base>1-incr {b} {m} {n} 1<b 0≤m m+b≤n mb+1≤n [ m<n ] = m ∷[ ≤-refl , m<n ] [ m<n ]
base>1-incr {b} {m} {n} 1<b 0≤m m+b≤n mb+1≤n (x ∷[ m≤x , x<n ] xs) with suc x ≟ n
base>1-incr {b} {m} {n} 1<b 0≤m m+b≤n mb+1≤n (x ∷[ m≤x , x<n ] xs) | no 1+x≠n = suc x ∷[ ≤-step m≤x , ≤→< x<n 1+x≠n ] xs
base>1-incr {b} {m} 1<b 0≤m m+b≤n mb+1≤n (x ∷[ m≤x , x<n ] xs) | yes refl = m ∷[ ≤-refl , s≤s m≤x ] base>1-incr 1<b 0≤m m+b≤n mb+1≤n xs

--
--   A ── incr ⟶ A'
--   |             |
--  toℕ           toℕ
--   ↓             ↓
--   n ── suc ⟶ suc n
--

-- first attempt :p
-- unary-toℕ-hom : (a : PN 1 1 2) → suc (toℕ a) ≡ toℕ (base=1-incr (s≤s z≤n) (s≤s (s≤s z≤n)) a)
-- unary-toℕ-hom [ m<n ] = refl
-- unary-toℕ-hom (zero ∷[ () , x<n ] xs)
-- unary-toℕ-hom (suc zero ∷[ m≤x , x<n ] xs) = cong suc {!   !}
-- unary-toℕ-hom (suc (suc x) ∷[ m≤x , s≤s (s≤s ()) ] xs)

--------------------------------------------------------------------------------
--  Instances

private
  -- Unary
  Unary : Set
  Unary = PN 1 1 2

  u₀ : Unary
  u₀ = 1 ∷[ s≤s z≤n , s≤s (s≤s z≤n) ] 1 ∷[ s≤s z≤n , s≤s (s≤s z≤n) ] [ s≤s (s≤s z≤n) ]

  -- Binary
  Bin : Set
  Bin = PN 2 0 2

  b₀ : Bin
  b₀ = 1 ∷[ z≤n , s≤s (s≤s z≤n) ] 0 ∷[ z≤n , s≤s z≤n ] [ s≤s z≤n ]

  -- Zeroless Binary
  Bin+ : Set
  Bin+ = PN 2 1 3

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module Issue390 where

data main : Set where

ext: agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Prelude.List.Relations.Permutation where

open import Prelude.List.Base
open import Prelude.List.Relations.Any

data Permutation {a} {A : Set a} : List A → List A → Set a where
  []  : Permutation [] []
  _∷_ : ∀ {x xs ys} (i : x ∈ ys) → Permutation xs (deleteIx ys i) →
          Permutation (x ∷ xs) ys

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
module ASN1.BER where

open import Data.Word8 using (Word8; _==_) renaming (primWord8fromNat to to𝕎; primWord8toNat to from𝕎)
open import Data.ByteString using (ByteString; Strict; Lazy; null; pack; unpack; fromChunks; toStrict; unsafeHead; unsafeTail; unsafeSplitAt) renaming (length to BSlength)
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; _+_; _∸_; _≤?_)
open import Data.List using (List; []; _∷_; length; reverse; concatMap; foldl; map)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_)
open import Data.String using (String)
open import Relation.Nullary using (Dec; yes; no)
open import Function using (case_of_; const)

open import ASN1.Util
open import ASN1.Untyped

-- encode
module _ where
  encodeLen : Len → List Word8
  encodeLen n with n ≤? 127
  encodeLen n | yes p = to𝕎 n ∷ []
  encodeLen n | no ¬p = to𝕎 (128 + length ns) ∷ reverse ns where
    ns : List Word8
    ns = base256 n

  -- TODO: use WF induction
  {-# TERMINATING #-}
  encode : AST → List (ByteString Strict)
  encode (tlv t (constr vs)) = pack (constructed t ∷ encodeLen l) ∷ evs where
    evs : List (ByteString Strict)
    evs = concatMap encode vs
    l : ℕ
    l = foldl _+_ 0 (map BSlength evs)
  encode (tlv t (prim octets)) = pack (t ∷ encodeLen (BSlength octets)) ∷ octets ∷ []

  encode′ : AST → ByteString Lazy
  encode′ ast = fromChunks (encode ast)

  encode″ : AST → ByteString Strict
  encode″ ast = toStrict (encode′ ast)

-- decode
module _ where

  Stream = ByteString Strict

  StateT : (Set → Set) → Set → Set → Set
  StateT M S A = S → M (A × S)

  E : Set → Set
  E A = String ⊎ A

  M = StateT E Stream
  -- TODO: use std monad

  _>>=_ : ∀ {A B} → M A → (A → M B) → M B
  ma >>= f = λ st → case ma st of λ
    { (inj₁ err) → inj₁ err
    ; (inj₂ (a , st′)) → f a st′
    }
  _>>_ : ∀ {A B} → M A → M B → M B
  ma >> mb = ma >>= (const mb)

  return : ∀ {A : Set} → A → M A
  return a = λ st → inj₂ (a , st)

  get : M Stream
  get st = inj₂ (st , st)

  error : ∀ {A : Set} → String → M A
  error e = λ _ → inj₁ e

  head : M Word8
  head st with null st
  head st | false = inj₂ (unsafeHead st , unsafeTail st)
  head st | true = inj₁ "stream is empty"

  take : ℕ → M (ByteString Strict)
  take n st with n ≤? BSlength st
  take n st | yes _ = inj₂ (unsafeSplitAt n st)
  take n st | no _ = inj₁ "stream is small"

  getTag : M Tag
  getTag = head

  getLen : M Len
  getLen = do
    n ← head
    let n′ = from𝕎 n
    no _ ← return (n′ ≤? 127) where
      yes _ → return n′
    let k = n′ ∸ 128
    ns ← take k
    let n″ = (fromBase256 (unpack ns))
    no _ ← return (n″ ≤? 127) where
      yes _ → error "invalid len"
    return n″

  decode : M AST

  {-# TERMINATING #-}
  decodeTLVs : M (List AST)
  decodeTLVs = do
    st ← get
    false ← return (null st) where
      true → return []
    h ← decode
    t ← decodeTLVs
    return (h ∷ t)

  getValue : Tag → Len → M Value
  getValue tag len = do
    bs ← take len
    true ← return (is-constructed tag) where
      false → return (prim bs)
    inj₂ (vs , _) ← return (decodeTLVs bs) where
      inj₁ e → error e
    return (constr vs)

  decode = do
    t ← getTag
    l ← getLen
    v ← getValue t l
    return (tlv t v)
  -- TODO: check for non-empty stream tail after decode


text:
------------------------------------------------------------------------------
-- Conversion rules for the division
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Program.Division.ConversionRulesATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Program.Division.Division

----------------------------------------------------------------------

-- NB. These equations are not used by the ATPs. They use the official
-- equation.
private
  -- The division result when the dividend is minor than the
  -- the divisor.
  postulate div-x<y : ∀ {i j} → i < j → div i j ≡ zero
  {-# ATP prove div-x<y #-}

  -- The division result when the dividend is greater or equal than the
  -- the divisor.
  postulate div-x≮y : ∀ {i j} → i ≮ j → div i j ≡ succ₁ (div (i ∸ j) j)
  {-# ATP prove div-x≮y #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --safe #-}
module Sol01 where

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

fibAux : ℕ -> ℕ -> ℕ -> ℕ
fibAux a b 0 = a
fibAux a b (suc n) = fibAux b (a + b) n

fib2 : ℕ -> ℕ
fib2 = fibAux 0 1

fib : ℕ -> ℕ
fib 0 = 0
fib 1 = 1
fib (suc (suc n)) = fib (suc n) + fib n

lemma : ∀ (a b c d n : ℕ) → fibAux (a + c) (b + d) n ≡ fibAux a b n + fibAux c d n
lemma a b c d zero = refl
lemma a b c d (suc n) rewrite sym (+-assoc (a + c) b d) | +-assoc a c b | +-comm c b | sym (+-assoc a b c) | +-assoc (a + b) c d = lemma b (a + b) d (c + d) n

fibEq : (n : ℕ) -> fib2 n ≡ fib n
fibEq zero = refl
fibEq (suc zero) = refl
fibEq (suc (suc n)) rewrite lemma 0 1 1 1 n | fibEq n | fibEq (suc n) | +-comm (fib n) (fib (suc n)) = refl

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness --no-subtyping #-}

module Agda.Builtin.Reflection.External where

open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Agda.Builtin.String

postulate
  execTC : String → List String → String
         → TC (Σ Nat (λ _ → Σ String (λ _ → String)))

{-# BUILTIN AGDATCMEXEC execTC #-}

max_stars_repo_name: Saizan/agda

max_issues_repo_name: Saizan/agda

max_forks_repo_name: Saizan/agda


text:
open import Mockingbird.Forest using (Forest)

-- Russel’s Forest
module Mockingbird.Problems.Chapter15 {b ℓ} (forest : Forest {b} {ℓ}) where

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product using (_×_; _,_; ∃-syntax; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_$_; flip; case_of_; _⇔_; Equivalence; mk⇔)
open import Function.Equivalence.Reasoning renaming (begin_ to ⇔-begin_; _∎ to _⇔-∎)
open import Level using (_⊔_)
open import Relation.Binary using (_Respects_)
open import Relation.Nullary using (¬_)
open import Relation.Unary using (Pred)

open Forest forest
open import Mockingbird.Forest.Birds forest

⇔-¬ : ∀ {a b} {A : Set a} {B : Set b} → A ⇔ B → (¬ A) ⇔ (¬ B)
⇔-¬ A⇔B = record
  { f = λ ¬A b → ¬A (A⇔B.g b)
  ; g = λ ¬B a → ¬B (A⇔B.f a)
  ; cong₁ = λ p → ≡.cong _ p
  ; cong₂ = λ p → ≡.cong _ p
  } where
  module A⇔B = Equivalence A⇔B
  open import Relation.Binary.PropositionalEquality as ≡ using (cong)

⇔-↯ : ∀ {a} {A : Set a} → ¬ (A ⇔ (¬ A))
⇔-↯ {A = A} A⇔¬A = yes but no
  where
    _but_ = flip _$_

    no : ¬ A
    no A = Equivalence.f A⇔¬A A A

    yes : A
    yes = Equivalence.g A⇔¬A no

module _ {s} (Sings : Pred Bird s)
         (respects : Sings Respects _≈_) where
  private
    -- TODO: move to Mockingbird.Forest.Axiom(.ExcludedMiddle)?
    ExcludedMiddle : Set (b ⊔ s)
    ExcludedMiddle = ∀ x → Sings x ⊎ ¬ Sings x

    doubleNegation : ExcludedMiddle → ∀ x → ¬ ¬ Sings x → Sings x
    doubleNegation LEM x ¬¬x-sings with LEM x
    ... | inj₁ x-sings = x-sings
    ... | inj₂ ¬x-sings = ⊥-elim $ ¬¬x-sings ¬x-sings

    doubleNegation-⇔ : ExcludedMiddle → ∀ x → (¬ ¬ Sings x) ⇔ Sings x
    doubleNegation-⇔ LEM x = mk⇔ (doubleNegation LEM x) λ x-sings ¬x-sings → ¬x-sings x-sings

    respects-⇔ : ∀ {x y} → x ≈ y → Sings x ⇔ Sings y
    respects-⇔ x≈y = mk⇔ (respects x≈y) (respects (sym x≈y))

  problem₁ :
      ExcludedMiddle
    → ∃[ a ] (∀ x → Sings (a ∙ x) ⇔ Sings (x ∙ x))
    → (∀ x → ∃[ x′ ] (∀ y → Sings (x′ ∙ y) ⇔ (¬ Sings (x ∙ y))))
    → ⊥
  problem₁ LEM (a , is-a) neg =
    let (a′ , is-a′) = neg a

        a′a′-sings⇔¬a′a′-sings : Sings (a′ ∙ a′) ⇔ (¬ Sings (a′ ∙ a′))
        a′a′-sings⇔¬a′a′-sings = ⇔-begin
          Sings (a′ ∙ a′)      ⇔⟨ is-a′ a′ ⟩
          ¬ Sings (a ∙ a′)     ⇔⟨ ⇔-¬ $ is-a a′ ⟩
          (¬ Sings (a′ ∙ a′))  ⇔-∎

        a′a′-sings⇒¬a′a′-sings = Equivalence.f a′a′-sings⇔¬a′a′-sings
        ¬a′a′-sings⇒a′a′-sings = Equivalence.g a′a′-sings⇔¬a′a′-sings

        ↯ : ⊥
        ↯ = case LEM (a′ ∙ a′) of λ
          { (inj₁ a′a′-sings) → a′a′-sings⇒¬a′a′-sings a′a′-sings a′a′-sings
          ; (inj₂ ¬a′a′-sings) → ¬a′a′-sings (¬a′a′-sings⇒a′a′-sings ¬a′a′-sings)
          }
    in ↯

  -- A constructive proof of Russel’s paradox, not using the LEM.
  problem₁′ :
      ∃[ a ] (∀ x → Sings (a ∙ x) ⇔ Sings (x ∙ x))
    → (∀ x → ∃[ x′ ] (∀ y → Sings (x′ ∙ y) ⇔ (¬ Sings (x ∙ y))))
    → ⊥
  problem₁′ (a , is-a) neg =
    let (a′ , is-a′) = neg a

        a′a′-sings⇔¬a′a′-sings : Sings (a′ ∙ a′) ⇔ (¬ Sings (a′ ∙ a′))
        a′a′-sings⇔¬a′a′-sings = ⇔-begin
          Sings (a′ ∙ a′)      ⇔⟨ is-a′ a′ ⟩
          (¬ Sings (a ∙ a′))   ⇔⟨ ⇔-¬ $ is-a a′ ⟩
          (¬ Sings (a′ ∙ a′))  ⇔-∎

    in ⇔-↯ a′a′-sings⇔¬a′a′-sings

  problem₂ : ⦃ _ : HasSageBird ⦄
    → ExcludedMiddle
    → ∃[ N ] (∀ x → Sings x ⇔ (¬ Sings (N ∙ x)))
    → ⊥
  problem₂ LEM (N , is-N) = isNotFond isFond
    where
      isFond : N IsFondOf (Θ ∙ N)
      isFond = isSageBird N

      isNotFond : ¬ N IsFondOf (Θ ∙ N)
      isNotFond isFond with LEM (Θ ∙ N)
      ... | inj₁ ΘN-sings = Equivalence.f (is-N (Θ ∙ N)) ΘN-sings (respects (sym isFond) ΘN-sings)
      ... | inj₂ ¬ΘN-sings =
        let N[ΘN]-sings : Sings (N ∙ (Θ ∙ N))
            N[ΘN]-sings = doubleNegation LEM (N ∙ (Θ ∙ N)) $
              Equivalence.f (⇔-¬ (is-N (Θ ∙ N))) ¬ΘN-sings
        in Equivalence.f (is-N (Θ ∙ N)) (respects isFond N[ΘN]-sings) N[ΘN]-sings

  -- A constructive proof of problem 2, not using the LEM.
  problem₂′ : ⦃ _ : HasSageBird ⦄
    → ∃[ N ] (∀ x → Sings x ⇔ (¬ Sings (N ∙ x)))
    → ⊥
  problem₂′ (N , is-N) = ⇔-↯ ΘN-sings⇔¬ΘN-sings
    where
      isFond : N IsFondOf (Θ ∙ N)
      isFond = isSageBird N

      ΘN-sings⇔¬ΘN-sings : Sings (Θ ∙ N) ⇔ (¬ Sings (Θ ∙ N))
      ΘN-sings⇔¬ΘN-sings = ⇔-begin
        Sings (Θ ∙ N)          ⇔⟨ is-N (Θ ∙ N) ⟩
        ¬ Sings (N ∙ (Θ ∙ N))  ⇔⟨ ⇔-¬ $ respects-⇔ isFond ⟩
        (¬ Sings (Θ ∙ N))      ⇔-∎

  problem₃ : ⦃ _ : HasSageBird ⦄
    → ∃[ A ] (∀ x y → Sings (A ∙ x ∙ y) ⇔ (¬ Sings x × ¬ Sings y))
    → ⊥
  problem₃ (A , is-A) = ↯
    where
      isFond : ∀ {x} → A ∙ x IsFondOf (Θ ∙ (A ∙ x))
      isFond {x} = isSageBird (A ∙ x)

      ¬Θ[Ax]-sings : ∀ x → ¬ Sings (Θ ∙ (A ∙ x))
      ¬Θ[Ax]-sings x Θ[Ax]-sings =
        let Ax[Θ[Ax]]-sings : Sings (A ∙ x ∙ (Θ ∙ (A ∙ x)))
            Ax[Θ[Ax]]-sings = respects (sym isFond) Θ[Ax]-sings

            ¬Θ[Ax]-sings : ¬ Sings (Θ ∙ (A ∙ x))
            ¬Θ[Ax]-sings = proj₂ $ Equivalence.f (is-A x (Θ ∙ (A ∙ x))) Ax[Θ[Ax]]-sings
        in ¬Θ[Ax]-sings Θ[Ax]-sings

      ¬¬x-sings : ∀ x → ¬ ¬ Sings x
      ¬¬x-sings x ¬x-sings =
        let Ax[Θ[Ax]]-sings = Equivalence.g (is-A x (Θ ∙ (A ∙ x))) (¬x-sings , ¬Θ[Ax]-sings x)
            Θ[Ax]-sings = respects isFond Ax[Θ[Ax]]-sings
        in ¬Θ[Ax]-sings x Θ[Ax]-sings

      ↯ : ⊥
      ↯ = ¬¬x-sings (Θ ∙ (A ∙ A)) $ ¬Θ[Ax]-sings A

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
-- Disjoint sum type; also used as logical disjunction.

{-# OPTIONS --safe #-}

module Tools.Sum where

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

-- Idempotency.

id : ∀ {A} → A ⊎ A → A
id (inj₁ x) = x
id (inj₂ x) = x

-- Symmetry.

sym : ∀ {A B} → A ⊎ B → B ⊎ A
sym (inj₁ x) = inj₂ x
sym (inj₂ x) = inj₁ x

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
mutual

  record R (A : Set) : Set where
    inductive
    field
      f₁ : A
      f₂ : R′ A

  record R′ (A : Set) : Set where
    inductive
    field
      f : R A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.Equiv.Induced-Poly where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.Polynomials.Univariate.Base

open import Cubical.Algebra.Polynomials.Multivariate.Base
open import Cubical.Algebra.Polynomials.Multivariate.Properties
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly
open Nth-Poly-structure

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- Lift

open IsRingHom

makeCommRingHomPoly : (A' B' : CommRing ℓ) → (f : CommRingHom A' B') → (n : ℕ) → CommRingHom (PolyCommRing A' n) (PolyCommRing B' n)
fst (makeCommRingHomPoly A' B' (f , fcrhom) n) = Poly-Rec-Set.f A' n (Poly B' n) trunc
                                     0P
                                     (λ v a → base v (f a))
                                     _Poly+_
                                     Poly+-assoc
                                     Poly+-Rid
                                     Poly+-comm
                                     (λ v → (cong (base v) (pres0 fcrhom)) ∙ (base-0P v))
                                     λ v a b → (base-Poly+ v (f a) (f b)) ∙ (cong (base v) (sym (pres+ fcrhom a b)))
snd (makeCommRingHomPoly A' B' (f , fcrhom) n) = makeIsRingHom
                          (cong (base (replicate zero)) (pres1 fcrhom))
                          (λ P Q → refl)
                          (Poly-Ind-Prop.f A' n _ (λ P p q i Q j → trunc _ _ (p Q) (q Q) i j)
                          (λ Q → refl)
                          (λ v a → Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
                                    refl
                                    (λ v' a' → cong (base (v +n-vec v')) (pres· fcrhom a a'))
                                    λ {U V} ind-U ind-V → cong₂ _Poly+_ ind-U  ind-V)
                           λ {U V} ind-U ind-V Q → cong₂ _Poly+_ (ind-U Q) (ind-V Q))

-----------------------------------------------------------------------------
-- Lift preserve equivalence

open RingEquivs

lift-equiv-poly : (A' B' : CommRing ℓ) → (e : CommRingEquiv A' B') → (n : ℕ) → CommRingEquiv (PolyCommRing A' n) (PolyCommRing B' n)
fst (lift-equiv-poly A' B' e n) = isoToEquiv is
  where
    et = fst e
    fcrh = snd e
    f = fst et
    g = invEq et
    gcrh : IsRingHom (snd (CommRing→Ring B')) g (snd (CommRing→Ring A'))
    gcrh = isRingHomInv (et , fcrh)

    is : Iso _ _
    Iso.fun is = fst (makeCommRingHomPoly A' B' (f , fcrh) n)
    Iso.inv is = fst (makeCommRingHomPoly B' A' (g , gcrh) n)
    Iso.rightInv is = (Poly-Ind-Prop.f B' n _ (λ _ → trunc _ _)
                      refl
                      (λ v a → cong (base v) (secEq et a))
                      λ {U V} ind-U ind-V → cong₂ _Poly+_ ind-U ind-V)
    Iso.leftInv is = (Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
                     refl
                     (λ v a → cong (base v) (retEq et a))
                     λ {U V} ind-U ind-V → cong₂ _Poly+_ ind-U ind-V)
snd (lift-equiv-poly A' B' e n) = snd (makeCommRingHomPoly A' B' (fst (fst e) , snd e) n)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module FFI where

open import Common.Prelude

_+'_ : Nat → Nat → Nat
zero +' y = y
suc x +' y = suc (x +' y)
{-# COMPILE GHC _+'_ = (+) :: Integer -> Integer -> Integer #-}

-- on-purpose buggy haskell implementation!
_+''_ : Nat → Nat → Nat
zero +'' y = y
suc x +'' y = suc (x +'' y)
{-# COMPILE GHC _+''_ = (-) :: Integer -> Integer -> Integer #-}

listMap : {A B : Set} → (A → B) → List A → List B
listMap f [] = []
listMap f (x ∷ xs) = f x ∷ listMap f xs

{-# COMPILE GHC listMap as listMap #-}
{-# FOREIGN GHC
  agdaMap :: (a -> b) -> [a] -> [b]
  agdaMap = listMap () ()
#-}

open import Common.IO
open import Common.Unit

_>>_ : {A B : Set} → IO A → IO B → IO B
m >> m' = m >>= λ _ → m'

main : IO Unit
main = do
  printNat (10 +' 5)
  printNat (30 +'' 7)


text:
------------------------------------------------------------------------------
-- Testing an implicit argument for natural numbers induction
------------------------------------------------------------------------------

{-# OPTIONS --allow-unsolved-metas     #-}
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.PA.Inductive.ImplicitArgumentInductionSL where

open import Data.Nat renaming ( suc to succ )
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------------

succCong : ∀ {m n} → m ≡ n → succ m ≡ succ n
succCong refl = refl

-- N.B. It is not possible to use an implicit argument in the
-- inductive hypothesis.
ℕ-ind : (A : ℕ → Set) → A zero → (∀ {n} → A n → A (succ n)) → ∀ n → A n
ℕ-ind A A0 h zero     = A0
ℕ-ind A A0 h (succ n) = h (ℕ-ind A A0 h n)

+-assoc : ∀ m n o → m + n + o ≡ m + (n + o)
+-assoc m n o = ℕ-ind A A0 is m
  where
  A : ℕ → Set
  A i = i + n + o ≡ i + (n + o)

  A0 : A zero
  A0 = refl

  is : ∀ {i} → A i → A (succ i)
  is ih = succCong ih


text:
{-# OPTIONS --no-main #-}

postulate
  easy : (A : Set₁) → A

record R₁ : Set₂ where
  field
    A : Set₁

record R₂ : Set₂ where
  field
    r₁ : R₁
    a  : R₁.A r₁

r₁ : R₁
r₁ .R₁.A = Set

r₂ : R₂
r₂ = λ where
  .R₂.r₁ → r₁
  .R₂.a  → easy _

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --rewriting #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

data Box : Set → Set₁ where
  box : (A : Set) → Box A

data D (A : Set) : Set₁ where
  c : A → Box A → D A

postulate
  any : {A : Set} → A
  one : {A : Set} → D A
  rew : ∀ A → c any (box A) ≡ one

-- Jesper, 2020-06-17: Ideally Agda should reject the above rewrite
-- rule, since it causes reduction to be unstable under eta-conversion
works : c any (box ⊤) ≡ c tt (box ⊤)
works = refl

-- However, currently it is accepted, breaking subject reduction:
{-# REWRITE rew #-}

fails : c any (box ⊤) ≡ c tt (box ⊤)
fails = refl

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --cubical --safe #-}

module Cubical.Data.Strict2Group.Explicit.ToXModule where

open import Cubical.Foundations.Prelude hiding (comp)

open import Cubical.Data.Group.Base
open import Cubical.Data.XModule.Base
open import Cubical.Data.Group.Action.Base
open import Cubical.Data.Sigma

open import Cubical.Data.Strict2Group.Explicit.Base
open import Cubical.Data.Strict2Group.Explicit.Interface

Strict2GroupExp→XModuleExp : {ℓ : Level} (S : Strict2GroupExp ℓ) → (XModuleExp ℓ)
Strict2GroupExp→XModuleExp (strict2groupexp C₀ C₁ s t i ∘ si ti s∘ t∘ isMorph∘ assoc∘ lUnit∘ rUnit∘) =
  record
    { G = C₀ ;
    H = ks ;
    τ = tₖₛ ;
    α = laction
      (λ g h → lAction.act lad (id g) h)
      (λ h →
         ΣPathP (p1 h ,
           isProp→PathP
             (λ i → snd (P (p1 h i)))
             (kerIsNormal {G = C₁} {H = C₀} s (id 1₀) h)
             (kerIsNormal {G = C₁} {H = C₀} s 1₁ h))
         ∙ lAction.identity lad h)
      (λ g g' h →
         ΣPathP (p2 g g' h ,
           isProp→PathP
             (λ i → snd (P (p2 g g' h i)))
             (kerIsNormal {G = C₁} {H = C₀} s (id (g ∙₀ g')) h)
             (kerIsNormal {G = C₁} {H = C₀} s (id g ∙₁ id g') h))
         ∙ (lAction.coh lad (id g) (id g') h))
      λ g h h' → lAction.hom lad (id g) h h' ;
    equivar = equivar ;
    peiffer = pf }
      where
        S = strict2groupexp C₀ C₁ s t i ∘ si ti s∘ t∘ isMorph∘ assoc∘ lUnit∘ rUnit∘
        open S2GInterface S
        -- the kernel of the source map
        kers = ker {G = C₁} {H = C₀} s
        -- the family of propositions ker(x) ≡ 1
        P = Subgroup.typeProp kers
        -- kernel coerced to group
        ks = Subgroup→Group {G = C₁} kers

        -- the left adjoint action of hom on its normal subgroup ker(src)
        lad : lAction C₁ ks
        lad = lActionAdjSubgroup C₁ kers (kerIsNormal {G = C₁} {H = C₀} s)

        -- the target map restricted to ker(src)
        tₖₛ = restrictGroupMorph {G = C₁} {H = C₀} t kers
        tarₖₛ = fst tₖₛ
        tar∙ₖₛ = snd tₖₛ
        -- multiplication, inverse in ker src
        _∙₁ₖₛ_ = isGroup.comp (Group.groupStruc ks)
        ks⁻¹ = isGroup.inv (Group.groupStruc ks)
        -- group laws in ker(src)
        lUnitₖₛ = isGroup.lUnit (Group.groupStruc ks)
        rUnitₖₛ = isGroup.rUnit (Group.groupStruc ks)
        rCancelₖₛ = isGroup.rCancel (Group.groupStruc ks)
        assocₖₛ = isGroup.assoc (Group.groupStruc ks)
        1ₖₛ = isGroup.id (Group.groupStruc ks)

        -- Composition restricted to ks×₀ks
        ∘ₖₛ : (g f : Group.type ks) → (src (fst g) ≡ tarₖₛ f) → Group.type ks
        ∘ₖₛ g f coh = (⊙' (fst g) (fst f) coh) , ((src⊙' (fst g) (fst f) coh) ∙ snd f)

        -- right and left unit law for restricted ∘
        abstract
          rUnit∘ₖₛ : (h : Group.type ks) →
            ∘ₖₛ h (id (src (fst h)) , si (src (fst h)) ∙ snd h)
              (sym (ti (src (fst h)))) ≡ h
          rUnit∘ₖₛ h = ΣPathP (rUnit∘ (fst h) ,
            isProp→PathP
              (λ i → snd (P (rUnit∘ (fst h) i)))
              (src⊙' (fst h) (id (src (fst h))) (sym (ti (src (fst h)))) ∙ si (src (fst h)) ∙ snd h)
              (snd h))
        abstract
          lUnit∘ₖₛ : (h : Group.type ks) →
            (⊙ (co (id (tar (fst h))) (fst h) (si (tar (fst h)))) , (src⊙' (id (tar (fst h))) (fst h) (si (tar (fst h)))) ∙ snd h) ≡ h
          lUnit∘ₖₛ h = ΣPathP (
            lUnit∘ (fst h) ,
            isProp→PathP
              (λ i → snd (P (lUnit∘ (fst h) i))) (src⊙' (id (tar (fst h))) (fst h) (si (tar (fst h))) ∙ snd h) (snd h))

        -- two proofs used in equivariant
        abstract
          p1 = λ (h : Group.type ks) → cong (λ z → (z ∙₁ fst h) ∙₁ (C₁⁻¹ z)) (morphId {G = C₀} {H = C₁} i)
          p2 = λ (g g' : Group.type C₀) (h : Group.type ks) → cong (λ z → (z ∙₁ fst h) ∙₁ (C₁⁻¹ z)) (id∙₀ g g')

          equivar = λ g h → tar∙₁ (id g ∙₁ fst h) (C₁⁻¹ (id g)) ∙∙
            cong (_∙₀ (tar (C₁⁻¹ (id g)))) (tar∙₁ (id g) (fst h)) ∙∙
            cong (((tar (id g)) ∙₀ (tar (fst h))) ∙₀_) (morphInv {G = C₁} {H = C₀} t (id g)) ∙
            cong (λ z → (z ∙₀ (tar (fst h))) ∙₀ (C₀⁻¹ z)) (ti g)

        -- the peiffer identity, proved according to
        -- ixh'ix- ≡ eixh'ix- ≡ hh-ixh'ix- ≡ hh-ixh'ixe

          pf : (h h' : Group.type ks) → lAction.act lad (id (tarₖₛ h)) h' ≡ (h ∙₁ₖₛ h') ∙₁ₖₛ (ks⁻¹ h)
          pf h h' =
            ixh'ix-
              ≡⟨ sym (lUnitₖₛ ixh'ix-) ⟩
            1ₖₛ ∙₁ₖₛ ixh'ix-
              ≡⟨ cong (_∙₁ₖₛ ixh'ix-) (sym (rCancelₖₛ h)) ⟩
            (h ∙₁ₖₛ h-) ∙₁ₖₛ ixh'ix-
              ≡⟨ assocₖₛ h h- ixh'ix- ⟩
            h ∙₁ₖₛ (h- ∙₁ₖₛ ixh'ix-)
              ≡⟨ cong (h ∙₁ₖₛ_) (
                h- ∙₁ₖₛ ixh'ix-
                  ≡⟨ cong (h- ∙₁ₖₛ_) (sym (rUnit∘ₖₛ ixh'ix-)) ⟩
                h- ∙₁ₖₛ (∘ₖₛ ixh'ix- (is ixh'ix-) (src≡tarIdSrc (fst ixh'ix-)))
                  ≡⟨ cong (_∙₁ₖₛ (∘ₖₛ ixh'ix- (is ixh'ix-) (src≡tarIdSrc (fst ixh'ix-)))) (sym (lUnit∘ₖₛ h-)) ⟩
                (⊙ ix-⊙h-₁ , (src⊙ ix-⊙h-₁) ∙ snd h-) ∙₁ₖₛ ∘ₖₛ ixh'ix- (is ixh'ix-) (src≡tarIdSrc (fst ixh'ix-))
                  ≡⟨ ΣPathP (q3 , isProp→PathP (λ i → snd (P (q3 i))) (snd ((ix-∘h-₁ , (src⊙ ix-⊙h-₁) ∙ snd h-) ∙₁ₖₛ ∘ₖₛ ixh'ix- (is ixh'ix-) (src≡tarIdSrc (fst ixh'ix-)))) (src⊙' (ix- ∙₁ fst ixh'ix-) (h- .fst ∙₁ fst (is ixh'ix-)) q1 ∙ q2)) ⟩
                (⊙ (co (ix- ∙₁ fst ixh'ix-) (h- .fst ∙₁ fst (is ixh'ix-)) q1)) , (src⊙' (ix- ∙₁ fst ixh'ix-) (h- .fst ∙₁ fst (is ixh'ix-)) q1) ∙ q2
                  ≡⟨ ΣPathP (q18 , (isProp→PathP (λ j → snd (P (q18 j))) ((src⊙' (ix- ∙₁ fst ixh'ix-) (h- .fst ∙₁ fst (is ixh'ix-)) q1) ∙ q2) ((src⊙' (ix- ∙₁ fst ixh'ix-) (h- .fst ∙₁ 1₁) (q5 ∙ q8)) ∙ q9))) ⟩
                (⊙ (co (ix- ∙₁ fst ixh'ix-) (h- .fst ∙₁ 1₁) (q5 ∙ q8))) ,
                  (src⊙' (ix- ∙₁ fst ixh'ix-) (h- .fst ∙₁ 1₁) (q5 ∙ q8)) ∙ q9
                  ≡⟨ ΣPathP (q17 , (isProp→PathP (λ j → snd (P (q17 j))) ((src⊙' (ix- ∙₁ fst ixh'ix-) (h- .fst ∙₁ 1₁) (q5 ∙ q8)) ∙ q9) ((src⊙' (ix- ∙₁ fst ixh'ix-) (fst h-) q5) ∙ snd h-))) ⟩
                (⊙ (co (ix- ∙₁ fst ixh'ix-) (h- .fst) q5)) ,
                  (src⊙' (ix- ∙₁ fst ixh'ix-) (h- .fst) q5)  ∙ snd h-
                  ≡⟨ ΣPathP (q16 , isProp→PathP (λ j → snd (P (q16 j))) ((src⊙' (ix- ∙₁ fst ixh'ix-) (fst h-) q5) ∙ snd h-) ((src⊙' (ix- ∙₁ fst ixh'ix-) (1₁ ∙₁ h- .fst) (q5 ∙ q6)) ∙ q7)) ⟩
                (⊙ (co (ix- ∙₁ fst ixh'ix-) (1₁ ∙₁ h- .fst) (q5 ∙ q6))) ,
                  (src⊙' (ix- ∙₁ fst ixh'ix-) (1₁ ∙₁ h- .fst) (q5 ∙ q6)) ∙ q7
                  ≡⟨ ΣPathP (q15 , (isProp→PathP (λ j → snd (P (q15 j))) ((src⊙' (ix- ∙₁ fst ixh'ix-) (1₁ ∙₁ h- .fst) (q5 ∙ q6)) ∙ q7) ((src⊙' ((fst h') ∙₁ ix-) (1₁ ∙₁ h- .fst) q4) ∙ q7))) ⟩
                (⊙ (co ((fst h') ∙₁ ix-) (1₁ ∙₁ h- .fst) q4)) ,
                  (src⊙' ((fst h') ∙₁ ix-) (1₁ ∙₁ h- .fst) q4) ∙ q7
                  ≡⟨ ΣPathP (q14 , isProp→PathP (λ j → snd (P (q14 j))) ((src⊙' ((fst h') ∙₁ ix-) (1₁ ∙₁ h- .fst) q4) ∙ q7) q12) ⟩
                (⊙ (co (fst h') 1₁ ((snd h') ∙ (sym tar1₁≡1₀)))) ∙₁ ix-∘h-₁ , q12
                  ≡⟨ ΣPathP (q11 , isProp→PathP (λ j → snd (P (q11 j))) q12 q13) ⟩
                h' .fst ∙₁ ix-∘h-₁ , q13
                  ≡⟨ ΣPathP (q10 , isProp→PathP (λ j → snd (P (q10 j)))
                    (src∙₁ (fst h') ix-∘h-₁ ∙∙
                      (λ i₁ → snd h' i₁ ∙₀ src ix-∘h-₁) ∙∙
                      lUnit₀ (src ix-∘h-₁) ∙∙
                      src⊙ ix-⊙h-₁ ∙∙
                      snd h-)
                    (Subgroup.compClosed kers h' h-)) ⟩
                h' .fst ∙₁ h- .fst , Subgroup.compClosed kers h' h- ≡⟨ refl ⟩
                (h' ∙₁ₖₛ h-) ≡⟨ refl ⟩ refl ) ⟩
              h ∙₁ₖₛ (h' ∙₁ₖₛ h-)
              ≡⟨ sym (assocₖₛ h h' h-) ⟩
            (h ∙₁ₖₛ h') ∙₁ₖₛ h- ≡⟨ refl ⟩ refl
            where
              -- some abbreviations
            h- = ks⁻¹ h -- h⁻¹
            x = tarₖₛ h -- target of h
            x- = tarₖₛ h- -- target of h⁻¹
            x-≡x⁻¹ : x- ≡ C₀⁻¹ x
            x-≡x⁻¹ = morphInv {G = ks} {H = C₀} tₖₛ h
            ix = id x -- i (t h)
            ix- = id x- -- i (t h⁻¹)
            ixh'ix- : Group.type ks -- abv. for (ix ∙₁ h') ∙₁ ix-
            ixh'ix- = lAction.act lad (id (tarₖₛ h)) h'
            is : Group.type ks → Group.type ks -- abv. for i(s _) in ks
            is h = id (src (fst h)) , (si (src (fst h))) ∙ snd h
            ix-⊙h-₁ = co ix- (fst h-) (si x-)
            ix-∘h-₁ = ⊙ ix-⊙h-₁

            -- some identities
            ix-≡ix⁻¹ : ix- ≡ (C₁⁻¹ ix)
            ix-≡ix⁻¹ = (cong id x-≡x⁻¹) ∙ (morphInv {G = C₀} {H = C₁} i x)
            ish≡1ₖₛ : (h : Group.type ks) → (is h) ≡ 1ₖₛ
            ish≡1ₖₛ h =
              ΣPathP
                (cong (fst i) (snd h) ∙ id1₀≡1₁ ,
                isProp→PathP
                  (λ j → snd (P (((λ k → id(snd h k)) ∙ id1₀≡1₁) j)))
                  (si (src (fst h)) ∙ snd h)
                  (Subgroup.subId kers))
            -- t h⁻¹ ≡ (t h)⁻¹
            th-≡x- = morphInv {G = ks} {H = C₀} tₖₛ h

            -----------------------------------------
            -- here comes particles of the main proof
            -----------------------------------------

            -- coherence condition for the composition
            -- ∘ (ix- ∙₁ fst ixh'ix-) (h- .fst ∙₁ fst (is ixh'ix-))
            q1 =
              src∙₁ ix- (fst ixh'ix-) ∙∙
              cong (_∙₀ src (fst ixh'ix-)) (si x-) ∙∙
              cong (x- ∙₀_) (snd ixh'ix-) ∙∙
              rUnit₀ x- ∙∙
              th-≡x- ∙∙
              sym (rUnit₀ (C₀⁻¹ x)) ∙∙
              cong ((C₀⁻¹ x) ∙₀_) (sym ((ti ((src (fst ixh'ix-)))) ∙ (snd ixh'ix-))) ∙∙
              cong (_∙₀ (tar (fst (is ixh'ix-)))) (sym th-≡x-) ∙∙
              sym (tar∙₁ (fst h-) (fst (is ixh'ix-)))

            -- to show that ∘ q1 is in ks, p2 is proof that f is in ks
            q2 = src∙₁ (fst h-) (fst (is ixh'ix-)) ∙∙
              cong (_∙₀ (src (fst (is ixh'ix-)))) (snd h-) ∙∙
              lUnit₀ (src (fst (is ixh'ix-))) ∙∙
              cong (λ z → src (fst z)) (ish≡1ₖₛ ixh'ix-) ∙∙
              snd 1ₖₛ

            -- (∘ (si x-)) ∙₁ (fst (∘ₖₛ (src≡tarIdSrc (fst ixh'ix-)))) ≡ ∘ q1
            q3 =
              (ix-∘h-₁ ∙₁ fst (∘ₖₛ ixh'ix- (is ixh'ix-) (src≡tarIdSrc (fst ixh'ix-)))) ≡⟨ refl ⟩
              ⊙ ix-⊙h-₁ ∙₁ ⊙ co3
                ≡⟨ sym (isMorph⊙ ix-⊙h-₁ co3) ⟩
              ⊙ (ix-⊙h-₁ ∙Co co3)
                ≡⟨ ⊙≡c (ix-⊙h-₁ ∙Co co3) q1 ⟩
              ⊙ co1 ≡⟨ refl ⟩ refl
              where
                co1 = co (ix- ∙₁ fst ixh'ix-) (fst h- ∙₁ fst (is ixh'ix-)) q1
                co3 = co (fst ixh'ix-) (fst (is ixh'ix-)) (src≡tarIdSrc (fst ixh'ix-))

            -- coherence condition for ∘ {g = ?} {f = 1₁ ∙₁ h- .fst} (_∙ q6)
            q6 = sym (lUnit₀ (tar (fst h-))) ∙∙
                 sym (cong (_∙₀ (tar (fst h-))) (morphId {G = C₁} {H = C₀} t)) ∙∙
                 sym (tar∙₁ 1₁ (fst h-))

            -- coherence condition for ∘ {g = (fst h') ∙₁ ix- } {f = 1₁ ∙₁ h- .fst } q4
            q4 =
              src∙₁ (fst h') ix- ∙∙
              (cong (_∙₀ src ix-) (snd h')) ∙∙
              lUnit₀ (src ix-) ∙∙
              si x- ∙∙
              q6

            -- coherence condition for ∘ {g = ix- ∙₁ fst ixh'ix- } {f = ?} (q5 ∙ ?)
            q5 =
              src∙₁ ix- (fst ixh'ix-) ∙∙
              cong ((src ix-) ∙₀_) (snd ixh'ix-) ∙∙
              rUnit₀ (src ix-) ∙
              si x-

            -- proof that 1₁ ∙₁ h- .fst : ker s
            q7 = src∙₁ 1₁ (fst h-) ∙∙
              cong (src 1₁ ∙₀_) (snd h-) ∙∙
              rUnit₀ (src 1₁) ∙ src1₁≡1₀

            -- proof that s x- ≡ t (h- .fst ∙₁ 1₁)
            q8 = sym (rUnit₀ (tar (fst h-))) ∙∙
              (sym (cong ((tar (fst h-)) ∙₀_) tar1₁≡1₀)) ∙∙
              (sym (tar∙₁ (fst h-) 1₁))

            -- proof that h- .fst ∙₁ 1₁ : ker s
            q9 = src∙₁ (fst h-) 1₁ ∙∙
              cong (_∙₀ (src 1₁)) (snd h-) ∙∙
              lUnit₀ (src 1₁) ∙
              src1₁≡1₀

            -- proof that (h' .fst ∙₁ ix-∘h-₁) ≡ (h' .fst ∙₁ h- .fst)
            q10 = cong (h' .fst ∙₁_) (lUnit∘ (fst h-))

            -- proof that (h'∘1₁)∙₁ ix-∘h-₁ ≡ h' ∙₁ ix-∘h-₁
            q11 = cong (_∙₁ ix-∘h-₁)
                       (⊙≡ (co (fst h') 1₁ (snd h' ∙ sym tar1₁≡1₀)) (id (src (fst h')) , sym id1₀≡1₁ ∙ sym (cong id (snd h'))) ∙
                       rUnit⊙c
                         (fst h')
                         ((snd h' ∙ (λ i₁ → tar1₁≡1₀ (~ i₁))) ∙ cong tar ((λ i₁ → id1₀≡1₁ (~ i₁)) ∙ (λ i₁ → id (snd h' (~ i₁))))))

            q12 =
                src∙₁ ((⊙ (co (fst h') 1₁ ((snd h') ∙ sym tar1₁≡1₀)))) ix-∘h-₁ ∙∙
                cong (_∙₀ (src ix-∘h-₁)) ((src⊙' (fst h') 1₁ ((snd h') ∙ (sym tar1₁≡1₀))) ∙  src1₁≡1₀) ∙∙
                lUnit₀ (src ix-∘h-₁) ∙
                src⊙' ix- (fst h-) (si x-) ∙ snd h-

            q13 = src∙₁ (fst h') ix-∘h-₁ ∙∙
              cong (_∙₀ (src ix-∘h-₁)) (snd h') ∙∙
              lUnit₀ (src ix-∘h-₁) ∙∙
              src⊙' ix- (fst h-) (si x-) ∙∙
              snd h-

            q14 =
              ⊙' ((fst h') ∙₁ ix-) (1₁ ∙₁ h- .fst) q4
                ≡⟨ ⊙≡c~ q4 (𝒸 (co (fst h') 1₁ (snd h' ∙ (λ i₁ → tar1₁≡1₀ (~ i₁))) ∙Co ix-⊙h-₁)) ⟩
              ⊙' ((fst h') ∙₁ ix-) (1₁ ∙₁ (fst h-)) (𝒸 (co (fst h') 1₁ (snd h' ∙ (λ i₁ → tar1₁≡1₀ (~ i₁))) ∙Co ix-⊙h-₁))
                ≡⟨ isMorph⊙ (co (fst h') 1₁ (snd h' ∙ (λ i₁ → tar1₁≡1₀ (~ i₁)))) ix-⊙h-₁ ⟩
             -- (⊙' (fst h') 1₁ (snd h' ∙ (λ i₁ → tar1₁≡1₀ (~ i₁)))) ∙₁ ix-∘h-₁ ≡⟨ refl ⟩
              refl

            q15 = ≡⊙c* (q5 ∙ q6)
                  (cong (ix- ∙₁_) (assoc₁ ix (fst h') (C₁⁻¹ ix)) ∙∙
                    sym (assoc₁ ix- ix (fst h' ∙₁ C₁⁻¹ ix)) ∙∙
                    cong (λ z → (z ∙₁ ix) ∙₁ (fst h' ∙₁ C₁⁻¹ ix)) ix-≡ix⁻¹ ∙∙
                    cong (_∙₁ (fst h' ∙₁ C₁⁻¹ ix)) (lCancel₁ ix) ∙∙
                    lUnit₁ (fst h' ∙₁ C₁⁻¹ ix) ∙
                    cong (fst h' ∙₁_) (sym ix-≡ix⁻¹))
                  q4
              {- use this to see what's going on
              ⊙ co1
                ≡⟨ ≡⊙c* (q5 ∙ q6)
                  ((cong (ix- ∙₁_) (assoc₁ ix (fst h') (C₁⁻¹ ix))) ∙
                    sym (assoc₁ ix- ix (fst h' ∙₁ C₁⁻¹ ix)) ∙
                    cong (λ z → (z ∙₁ ix) ∙₁ (fst h' ∙₁ C₁⁻¹ ix)) ix-≡ix⁻¹ ∙
                    cong (_∙₁ (fst h' ∙₁ C₁⁻¹ ix)) (lCancel₁ ix) ∙
                    (lUnit₁ (fst h' ∙₁ C₁⁻¹ ix)) ∙
                    (cong (fst h' ∙₁_) (sym ix-≡ix⁻¹)))
                  q4 ⟩
              ⊙ co2 ≡⟨ refl ⟩ refl
              where
                co1 = co (ix- ∙₁ (fst ixh'ix-)) (1₁ ∙₁ (fst h-)) (q5 ∙ q6)
                co2 = co ((fst h') ∙₁ ix-) (1₁ ∙₁ (fst h-)) q4 -}

            q16 = ⊙≡c* q5 (sym (lUnit₁ (fst h-))) (q5 ∙ q6)
              {- use this to see what's going on
              ⊙ co1
                ≡⟨ ⊙≡c* q5 (sym (lUnit₁ (fst h-))) (q5 ∙ q6) ⟩
              ⊙ co2 ≡⟨ refl ⟩ refl
              where
                co1 = co (ix- ∙₁ fst ixh'ix-) (fst h-) q5
                co2 = co (ix- ∙₁ fst ixh'ix-) (1₁ ∙₁ fst h-) (q5 ∙ q6) -}

            q17 = ⊙≡c* (q5 ∙ q8) (rUnit₁ (fst h-)) q5
              {- use this to see what's going on
              ⊙ co1
                ≡⟨ ⊙≡c* (q5 ∙ q8) (rUnit₁ (fst h-)) q5 ⟩
              ⊙ co2 ≡⟨ refl ⟩ refl
              where
                co1 = co (ix- ∙₁ fst ixh'ix-) (fst h- ∙₁ 1₁) (q5 ∙ q8)
                co2 = co (ix- ∙₁ fst ixh'ix-) (fst h-) q5 -}

            q18 = ⊙≡c* q1 (cong (fst h- ∙₁_) ((cong id (snd ixh'ix-)) ∙ id1₀≡1₁)) (q5 ∙ q8)
              {- use this to see what's going on
              ⊙ co1 ≡⟨ ⊙≡c* q1 (cong (fst h- ∙₁_)
                ((cong id (snd ixh'ix-)) ∙ id1₀≡1₁))
                (q5 ∙ q8) ⟩
              ⊙ co2 ≡⟨ refl ⟩ refl
              where
                co1 = co (ix- ∙₁ fst ixh'ix-) (fst h- ∙₁ (fst (is ixh'ix-))) q1
                co2 = co (ix- ∙₁ fst ixh'ix-) (fst h- ∙₁ 1₁) (q5 ∙ q8) -}

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
module Test.Numeral where
import Lvl
open import Relator.Equals{Lvl.𝟎}

  module One where
    test0 : (0 mod 1) ≡ 0
    test0 = [≡]-intro

    test1 : (1 mod 1) ≡ 0
    test1 = [≡]-intro

    test2 : (2 mod 1) ≡ 0
    test2 = [≡]-intro

    test3 : (3 mod 1) ≡ 0
    test3 = [≡]-intro

    test4 : (4 mod 1) ≡ 0
    test4 = [≡]-intro

    test5 : (5 mod 1) ≡ 0
    test5 = [≡]-intro

    test6 : (6 mod 1) ≡ 0
    test6 = [≡]-intro

    test7 : (7 mod 1) ≡ 0
    test7 = [≡]-intro

    test8 : (8 mod 1) ≡ 0
    test8 = [≡]-intro

    test9 : (9 mod 1) ≡ 0
    test9 = [≡]-intro

    test10 : (10 mod 1) ≡ 0
    test10 = [≡]-intro

    test11 : (11 mod 1) ≡ 0
    test11 = [≡]-intro

  module Two where
    test0 : (0 mod 2) ≡ 0
    test0 = [≡]-intro

    test1 : (1 mod 2) ≡ 1
    test1 = [≡]-intro

    test2 : (2 mod 2) ≡ 0
    test2 = [≡]-intro

    test3 : (3 mod 2) ≡ 1
    test3 = [≡]-intro

    test4 : (4 mod 2) ≡ 0
    test4 = [≡]-intro

    test5 : (5 mod 2) ≡ 1
    test5 = [≡]-intro

    test6 : (6 mod 2) ≡ 0
    test6 = [≡]-intro

    test7 : (7 mod 2) ≡ 1
    test7 = [≡]-intro

    test8 : (8 mod 2) ≡ 0
    test8 = [≡]-intro

    test9 : (9 mod 2) ≡ 1
    test9 = [≡]-intro

    test10 : (10 mod 2) ≡ 0
    test10 = [≡]-intro

    test11 : (11 mod 2) ≡ 1
    test11 = [≡]-intro

  module Three where
    test0 : (0 mod 3) ≡ 0
    test0 = [≡]-intro

    test1 : (1 mod 3) ≡ 1
    test1 = [≡]-intro

    test2 : (2 mod 3) ≡ 2
    test2 = [≡]-intro

    test3 : (3 mod 3) ≡ 0
    test3 = [≡]-intro

    test4 : (4 mod 3) ≡ 1
    test4 = [≡]-intro

    test5 : (5 mod 3) ≡ 2
    test5 = [≡]-intro

    test6 : (6 mod 3) ≡ 0
    test6 = [≡]-intro

    test7 : (7 mod 3) ≡ 1
    test7 = [≡]-intro

    test8 : (8 mod 3) ≡ 2
    test8 = [≡]-intro

    test9 : (9 mod 3) ≡ 0
    test9 = [≡]-intro

    test10 : (10 mod 3) ≡ 1
    test10 = [≡]-intro

    test11 : (11 mod 3) ≡ 2
    test11 = [≡]-intro

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K --safe #-}

module Relation.Binary.PropositionalEquality.FasterReasoning {a} {A : Set a} where

open import Relation.Binary.PropositionalEquality

infix  3 _∎
infixr 2 _≡⟨⟩_ step-≡ step-≡˘
infix  1 begin_

begin_ : ∀{x y : A} → x ≡ y → x ≡ y
begin_ x≡y = x≡y

_≡⟨⟩_ : (x {y} : A) → x ≡ y → x ≡ y
_ ≡⟨⟩ x≡y = x≡y

step-≡ : (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
step-≡ _ y≡z x≡y = trans x≡y y≡z

syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z

_∎ : (x : A) → x ≡ x
_∎ _ = refl

step-≡˘ : (x {y z} : A) → y ≡ z → y ≡ x → x ≡ z
step-≡˘ _ y≡z y≡x = trans (sym y≡x) y≡z

syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
module AbstractData where

abstract
  data D : Set where
    c : D

  d : D
  d = c


text:
-- ---------------------------------------------------------------------
--  Geometric Group Theory (topics from)
-- ------------------------------------------
-- actions are usually denoted as `·` (\cdot)
--  mimics structure in stdlib
-- ---------------------------------------------------------------------

module GGT where
open import GGT.Definitions public
open import GGT.Structures public
open import GGT.Bundles public

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt


text:
{-# OPTIONS --show-implicit #-}
{-# OPTIONS --sized-types #-}
{-# OPTIONS --termination-depth=2 #-}
-- {-# OPTIONS -v term:10 #-}

module SizedBTree where

open import Common.Size

data BTree (A : Set) : {size : Size} → Set where
  leaf : {i : Size} → A → BTree A {↑ i}
  node : {i : Size} → BTree A {i} → BTree A {i} → BTree A {↑ i}

map : ∀ {A B i} → (A → B) → BTree A {i} → BTree B {i}
map f (leaf a) = leaf (f a)
map f (node l r) = node (map f l) (map f r)

-- deep matching

deep : ∀ {i A} → BTree A {i} → A
deep (leaf a) = a
deep (node (leaf _) r) = deep r
deep (node (node l r) _) = deep (node l r)

-- nesting

deep2 : ∀ {i A} → BTree A {i} → BTree A {i}
deep2 (leaf a) = leaf a
deep2 (node (leaf _) r) = r
deep2 (node (node l r) t) with deep2 (deep2 (node l r))
... | leaf a = leaf a
... | node l2 r2 = deep2 (node l2 r2)

-- increasing the termination count does the job!

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{- Lemmas and operations involving rewriting and heterogeneous equality. -}
module TemporalOps.Common.Rewriting where

open import Relation.Binary.HeterogeneousEquality as ≅
open import Relation.Binary.PropositionalEquality as ≡

-- | Rewriting and heterogeneous equality

-- Substitution with identity predicate – explicit rewriting
rew : ∀{ℓ}{x y : Set ℓ} -> x ≡ y -> x -> y
rew refl x = x

-- Rewriting preserves heterogeneous equality
rew-to-≅ : ∀{ℓ}{A B : Set ℓ}{v : A} -> (p : A ≡ B) -> v ≅ rew p v
rew-to-≅ {A = A} {.A} {v} refl = ≅.refl

-- Heterogenous equality with differently typed arguments
-- can be converted to homogeneous equality via rewriting of the types
≅-to-rew-≡ : ∀ {P Q : Set} {x : P} {y : Q}
            -> (p : x ≅ y) -> (e : P ≡ Q)
            -> rew e x ≡ y
≅-to-rew-≡ ≅.refl refl = refl

-- Rewriting by p is cancelled out by rewriting by (sym p)
rew-cancel : ∀ {P Q : Set}
            -> (v : P) -> (p : P ≡ Q)
            -> rew (≡.sym p) (rew p v) ≡ v
rew-cancel v refl = refl

-- | Equality of equality proofs and functions
-- Two propositional equality proofs are propositionally (heterogeneously) equal
-- if given two heterogeneously equal values, rewriting each with
-- the respective proofs gives propositionally (heterogeneously) equal terms.

-- Propositional equality of equality proofs
Proof-≅ : ∀{p1 p2 q1 q2 : Set} -> p1 ≡ q1 -> p2 ≡ q2 -> Set
Proof-≅ {p1}{p2} pf1 pf2 =
        (v : p1) (v′ : p2) -> v ≅ v′ -> rew pf1 v ≅ rew pf2 v′

-- Propositional equality of equality proofs
Proof-≡ : ∀{p1 p2 q : Set} -> p1 ≡ q -> p2 ≡ q -> Set
Proof-≡ {p1}{p2} pf1 pf2 =
        (v : p1) (v′ : p2) -> v ≅ v′ -> rew pf1 v ≡ rew pf2 v′

-- Propositional equality of functions
Fun-≅ : ∀{a1 a2 b1 b2 : Set} -> (a1 -> b1) -> (a2 -> b2) -> Set
Fun-≅ {a1}{a2} f1 f2 =
        (v : a1) (v′ : a2) -> v ≅ v′ -> f1 v ≅ f2 v′

-- | Other lemmas

-- Heterogeneous congruence of three arguments
≅-cong₃ : ∀ {a b c d} {A : Set a} {B : A → Set b} {C : ∀ (x : A) → B x → Set c}
            {D : ∀ (x : A) -> (y : B x) -> C x y -> Set d} {x y z w u v}
       -> (f : (x : A) (y : B x) (z : C x y) → D x y z)
       -> x ≅ y -> z ≅ w -> u ≅ v -> f x z u ≅ f y w v
≅-cong₃ f ≅.refl ≅.refl ≅.refl = ≅.refl

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module Issue546 where

data I : Set where
  i : I

data ⊤ : Set where
  tt : ⊤

abstract
  P : I → Set
  P i = ⊤

Q : P i → Set
Q _ = ⊤

q : Q tt
q = tt

-- Q tt should be rejected.

-- This bug was introduced in Agda 2.3.0.

max_forks_repo_name: masondesu/agda


text:
open import Prelude hiding (id; Bool)

module Implicits.Resolution.Deterministic.Incomplete where

open import Implicits.Syntax
open import Implicits.WellTyped
open import Implicits.Substitutions

open import Data.Product
open import Data.List hiding ([_])
open import Data.List.Any
open Membership-≡
open import Extensions.ListFirst

Bool : Type 0
Bool = simpl $ tc 0

Int : Type 0
Int = simpl $ tc 1

-- We'll proof incompleteness with a simple example that we'll be able to resolve
-- using the ambigous resolution rules, but not with the deterministic rules.
-- This proofs that the ambiguous rules are stronger, such that together with Oliveira's
-- proof that determinstic resolution is sound w.r.t. ambiguous resolution, we have the
-- result that deterministic resolution is incomplete (or ambiguous resolution is strictly stronger)

Δ : ICtx 0
Δ = (Int ⇒ Bool) ∷ Bool List.∷ List.[]

open import Implicits.Resolution.Deterministic.Resolution as D
open import Implicits.Resolution.Ambiguous.Resolution as A
open import Extensions.ListFirst

private
  -- proof that Bool is not derivable under the deterministic resolution rules
  deterministic-cant : ¬ (Δ D.⊢ᵣ Bool)
  deterministic-cant (r-simp fst fst↓bool) with
    FirstLemmas.first-unique (here (m-iabs m-simp) (Bool List.∷ List.[])) fst
  deterministic-cant (r-simp fst (i-iabs (r-simp r _) b)) | refl = ¬r◁Int (, r)
    where
      ¬r◁Int : ¬ (∃ λ r → Δ ⟨ tc 1 ⟩= r)
      ¬r◁Int (._ , here (m-iabs ()) ._)
      ¬r◁Int (._ , there _ _ (here () .List.[]))
      ¬r◁Int ( _ , there _ _ (there _ _ ()))

  -- proof that Bool is derivable under the "Ambiguous" resolution rules
  ambiguous-can : Δ A.⊢ᵣ Bool
  ambiguous-can = r-ivar (there (here refl))

incomplete : ∃ λ ν → ∃₂ λ (Δ : ICtx ν) r → (Δ A.⊢ᵣ r) × (¬ Δ D.⊢ᵣ r)
incomplete = , (Δ , (Bool , (ambiguous-can , deterministic-cant)))


text:
module Issue676 where

data Bool : Set where
  true false : Bool

data ⊥ : Set where

data Silly A : Set where
  [_]  : A → Silly A
  fail : ⊥ → Silly A

-- This shouldn't be projection-like since the second clause won't reduce.
unsillify : ∀ {A} → Silly A → A
unsillify [ x ] = x
unsillify (fail ())

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

-- Triggers an __IMPOSSIBLE__ if unsillify is projection like.
bad : (x : ⊥) → unsillify (fail x) ≡ true
bad x = refl


text:
module Coirc.Format where
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Char
open import Data.String
open import Data.List
open import Data.Sum
open import Data.Product
open import Coirc

infixr 3 _∣_
infixr 1 _>>_ _>>-_ _>>=_

within? : Char → ℕ → ℕ → Bool
within? c start end = toBool lower ∧ toBool higher
  where
  target = toNat c
  lower  = suc target ∸ start
  higher = suc end ∸ target
  toBool : ℕ → Bool
  toBool zero    = false
  toBool (suc _) = true

data DarRange (start end : ℕ) : Bool → Set where
  dar : (c : Char) → DarRange start end (within? c start end)

data Dar : ℕ → Set where
  dar : (c : Char) → Dar (toNat c)

data U : Set where
  CHAR : U
  DAR : ℕ → U
  DAR-RANGE : ℕ → ℕ → U
  `*! `*sp `*crlf : U

El : U → Set
El CHAR = Char
El (DAR n) = Dar n
El (DAR-RANGE n m) = DarRange n m true
El `*! = String
El `*sp = String
El `*crlf = String

mutual
  data Format : Set where
    Fail End : Format
    As : Event → Format
    Base : U → Format
    Skip Or And : Format → Format → Format
    Use : (f : Format) → (⟦ f ⟧ → Format) → Format

  ⟦_⟧ : Format → Set
  ⟦ Fail ⟧ = ⊥
  ⟦ End ⟧ = ⊤
  ⟦ As _ ⟧ = Event
  ⟦ Base u ⟧ = El u
  ⟦ Skip _ f ⟧ = ⟦ f ⟧
  ⟦ Or f₁ f₂ ⟧ = ⟦ f₁ ⟧ ⊎ ⟦ f₂ ⟧
  ⟦ And f₁ f₂ ⟧ = ⟦ f₁ ⟧ × ⟦ f₂ ⟧
  ⟦ Use f₁ f₂ ⟧ = Σ ⟦ f₁ ⟧ λ x → ⟦ f₂ x ⟧

_>>_ : Format → Format → Format
f₁ >> f₂ = Skip f₁ f₂

_>>-_ : Format → Format → Format
x >>- y = And x y

_>>=_ : (f : Format) → (⟦ f ⟧ → Format) → Format
x >>= y = Use x y

_∣_ : Format → Format → Format
x ∣ y = Or x y

char : Char → Format
char c = Base (DAR (toNat c))

str : String → Format
str s = chars (toList s)
  where
  chars : List Char → Format
  chars [] = End
  chars (x ∷ xs) = char x >>- chars xs

DIGIT = Base (DAR-RANGE (toNat '0') (toNat '9'))
cl    = char ':'
sp    = char ' '
cr    = char '\r'
lf    = char '\n'
crlf  = cr >>- lf

prefix = cl >> Base `*sp

Notice : Format
Notice =
  prefix >>
  sp >>
  str "NOTICE" >>
  sp >> char '*' >> sp >>
  Base `*crlf >> -- text
  crlf >>
  As notice

NumericReply : Format
NumericReply =
  prefix >>
  sp >>
  (DIGIT >>- DIGIT >>- DIGIT) >>
  sp >>
  Base `*sp >> -- target
  sp >>
  Base `*crlf >> -- text
  crlf >>
  As numeric

Mode : Format
Mode =
  prefix >>
  sp >>
  str "MODE" >>
  sp >>
  Base `*sp >> -- nickname
  sp >>
  Base `*crlf >> -- modes
  crlf >>
  As mode

Ping : Format
Ping =
  str "PING" >>
  sp >>
  Base `*crlf >> -- server
  crlf >>
  As ping

Privmsg : Format
Privmsg =
  cl >>
  Base `*! >>= λ source →
  Base `*sp >>
  sp >>
  str "PRIVMSG" >>
  sp >>
  Base `*sp >> -- target
  sp >>
  cl >>
  Base `*crlf >>= λ text →
  crlf >>
  As (privmsg source text)

max_stars_repo_name: larrytheliquid/coirc

max_issues_repo_name: larrytheliquid/coirc

max_forks_repo_name: larrytheliquid/coirc


text:
------------------------------------------------------------------------
-- Termination predicates
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --sized-types #-}

open import Prelude hiding (↑; module W)

module Delay-monad.Alternative.Termination {a} {A : Type a} where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)

open import Equality.Decision-procedures equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
  as Trunc
import Nat equality-with-J as N

open import Delay-monad hiding (Delay)
open import Delay-monad.Alternative
open import Delay-monad.Alternative.Equivalence
open import Delay-monad.Alternative.Properties
import Delay-monad.Bisimilarity as B
import Delay-monad.Termination as T

infix 4 _⇓_ _∥⇓∥_ _⇓′_

-- The three logically equivalent types x ⇓ y, x ∥⇓∥ y and x ⇓′ y
-- all mean that the computation x terminates with the value y:
--
-- ∙ _⇓_ is the "obvious" definition. The definition does not
--   involve truncation, and can be used directly.
--
-- ∙ _∥⇓∥_ is a truncated variant of _⇓_. It may be more convenient
--   to construct values of type x ∥⇓∥ y than of type x ⇓ y, because
--   the former type is a proposition.
--
-- ∙ _⇓′_ is an auxiliary definition, used to prove that the other
--   two are logically equivalent. This definition does not use
--   truncation, but is still propositional (if A is a set).

_⇓_ : Delay A → A → Type a
(f , _) ⇓ y = ∃ λ n → f n ↓ y

_∥⇓∥_ : Delay A → A → Type a
x ∥⇓∥ y = ∥ x ⇓ y ∥

_⇓′_ : Delay A → A → Type _
(f , _) ⇓′ y = ∃ λ m → f m ↓ y × (∀ n → ¬ f n ↑ → m N.≤ n)

-- _⇓′_ is a family of propositions (if A is a set).

⇓′-propositional :
  Is-set A → ∀ x {y : A} → Is-proposition (x ⇓′ y)
⇓′-propositional A-set x@(f , _) {y} p q =
                     $⟨ number-unique p q ⟩
  proj₁ p ≡ proj₁ q  ↝⟨ ignore-propositional-component
                          (×-closure 1 (Maybe-closure 0 A-set)
                                       (Π-closure ext 1 λ _ →
                                        Π-closure ext 1 λ _ →
                                        ≤-propositional)) ⟩□
  p ≡ q              □
  where
  number-unique : (p q : x ⇓′ y) → proj₁ p ≡ proj₁ q
  number-unique (pm , f-pm↓y , pm≤) (qm , f-qm↓y , qm≤) =
    N.≤-antisymmetric
      (pm≤ qm λ f-qm↑ → ⊎.inj₁≢inj₂ (nothing  ≡⟨ sym f-qm↑ ⟩
                                     f qm     ≡⟨ f-qm↓y ⟩∎
                                     just y   ∎))
      (qm≤ pm λ f-pm↑ → ⊎.inj₁≢inj₂ (nothing  ≡⟨ sym f-pm↑ ⟩
                                     f pm     ≡⟨ f-pm↓y ⟩∎
                                     just y   ∎))

-- All values that a computation can terminate with are equal.

termination-value-unique :
  ∀ (x : Delay A) {y z} → x ⇓ y → x ⇓ z → y ≡ z
termination-value-unique (f , inc) {y} {z} (m , fm↓y) (n , fn↓z)
  with N.total m n
... | inj₁ m≤n = ⊎.cancel-inj₂
                   (just y  ≡⟨ sym (↓-upwards-closed inc m≤n fm↓y) ⟩
                    f n     ≡⟨ fn↓z ⟩∎
                    just z  ∎)
... | inj₂ n≤m = ⊎.cancel-inj₂
                   (just y  ≡⟨ sym fm↓y ⟩
                    f m     ≡⟨ ↓-upwards-closed inc n≤m fn↓z ⟩∎
                    just z  ∎)

-- _⇓_ is contained in _⇓′_.

⇓→⇓′ : ∀ x {y : A} → x ⇓ y → x ⇓′ y
⇓→⇓′ x@(f , inc) = uncurry find-min
  where
  find-min : ∀ {y} m → f m ↓ y → x ⇓′ y
  find-min     zero    f0↓y    = zero , f0↓y , λ _ _ → N.zero≤ _
  find-min {y} (suc m) f-1+m↓y with inspect (f m)
  ... | nothing , fm↑ = suc m , f-1+m↓y , 1+m-is-min
    where
    1+m-is-min : ∀ n → ¬ f n ↑ → m N.< n
    1+m-is-min n ¬fn↑ with inspect (f n)
    ... | nothing , fn↑ = ⊥-elim (¬fn↑ fn↑)
    ... | just _  , fn↓ = ↑<↓ inc fm↑ fn↓
  ... | just y′ , fm↓y′ =
             $⟨ find-min m fm↓y′ ⟩
    x ⇓′ y′  ↝⟨ Σ-map id (Σ-map with-other-value id) ⟩□
    x ⇓′ y   □
    where
    with-other-value : ∀ {n} → f n ↓ y′ → f n ↓ y
    with-other-value =
      subst (_ ↓_)
            (termination-value-unique x (_ , fm↓y′) (_ , f-1+m↓y))

-- _⇓_ and _∥⇓∥_ are pointwise logically equivalent (if A is a set).

⇓⇔∥⇓∥ : Is-set A → ∀ x {y : A} → x ⇓ y ⇔ x ∥⇓∥ y
⇓⇔∥⇓∥ A-set x {y} = record
  { to   = ∣_∣
  ; from = x ∥⇓∥ y  ↝⟨ Trunc.rec (⇓′-propositional A-set x) (⇓→⇓′ x) ⟩
           x ⇓′ y   ↝⟨ Σ-map id proj₁ ⟩□
           x ⇓ y    □
  }

-- The notion of termination defined here is logically equivalent
-- (via Delay⇔Delay) to the one defined for the coinductive delay
-- monad.

⇓⇔⇓ : ∀ x {y} → x ⇓ y ⇔ _⇔_.to Delay⇔Delay x T.⇓ y
⇓⇔⇓ x = record
  { to   = λ { (n , fn↓y) → to n _ (proj₂ x) refl fn↓y }
  ; from = from _ refl
  }
  where
  to : ∀ {f : ℕ → Maybe A} n x {y} →
       Increasing f →
       x ≡ f 0 → f n ↓ y → Delay⇔Delay.To.to′ f x T.⇓ y
  to (suc n) nothing f-inc f0↑ fn↓y =
    B.laterʳ (to n _ (f-inc ∘ suc) refl fn↓y)

  to {f} zero nothing {y} _ f0↑ fn↓y =
    ⊥-elim $ ⊎.inj₁≢inj₂ (
      nothing  ≡⟨ f0↑ ⟩
      f 0      ≡⟨ fn↓y ⟩∎
      just y   ∎)

  to {f} n (just x) {y} f-inc f0↓x fn↓y =
    subst (_ T.⇓_)
          (⊎.cancel-inj₂ {A = ⊤}
             (just x  ≡⟨ sym $ ↓-upwards-closed₀ f-inc (sym f0↓x) n ⟩
              f n     ≡⟨ fn↓y ⟩∎
              just y  ∎))
          B.now

  from : ∀ {f : ℕ → Maybe A} {y} x →
         x ≡ f 0 → Delay⇔Delay.To.to′ f x T.⇓ y → ∃ λ n → f n ↓ y
  from (just x) f0↓x B.now           = 0 , sym f0↓x
  from nothing  _    (B.laterʳ to⇓y) =
    Σ-map suc id (from _ refl to⇓y)

⇓⇔⇓′ : ∀ {x} {y : A} → x T.⇓ y ⇔ _⇔_.from Delay⇔Delay x ⇓ y
⇓⇔⇓′ = record
  { to   = to
  ; from = uncurry (from _)
  }
  where
  to : ∀ {x y} → x T.⇓ y → Delay⇔Delay.from x ⇓ y
  to B.now        = 0 , refl
  to (B.laterʳ p) = Σ-map suc id (to p)

  from : ∀ x {y} n → proj₁ (Delay⇔Delay.from x) n ↓ y → x T.⇓ y
  from (now x)   n       refl = B.now
  from (later x) zero    ()
  from (later x) (suc n) xn↓y = B.laterʳ (from (force x) n xn↓y)

-- If there is a function f : ℕ → Maybe A satisfying a property
-- similar to termination-value-unique, then this function can be
-- turned into a value in Delay A which is, in some sense, weakly
-- bisimilar to the function.

complete-function :
  (f : ℕ → Maybe A) →
  (∀ {y z} → (∃ λ m → f m ↓ y) → (∃ λ n → f n ↓ z) → y ≡ z) →
  ∃ λ x → ∀ {y} → x ⇓ y ⇔ ∃ λ n → f n ↓ y
complete-function f unique =
    (first-value , inc)
  , λ {y} → record
      { to   = (∃ λ n → first-value n ↓ y)  ↝⟨ uncurry first-value↓→f↓ ⟩□
               (∃ λ n → f n ↓ y)            □
      ; from = (∃ λ n → f n ↓ y)            ↝⟨ Σ-map id (f↓→first-value↓ _) ⟩□
               (∃ λ n → first-value n ↓ y)  □
      }
  where
  -- If f m terminates for some m smaller than or equal to n, then
  -- first-value n returns the value of f for the largest such m, and
  -- otherwise nothing.

  first-value : ℕ → Maybe A
  first-value zero    = f zero
  first-value (suc n) =
    Prelude.[ (λ _ → first-value n) , just ] (f (suc n))

  -- Some simple lemmas.

  step : ∀ {n} → f (suc n) ↑ → first-value (suc n) ≡ first-value n
  step {n} = cong Prelude.[ (λ _ → first-value n) , just ]

  done : ∀ {n y} → f (suc n) ↓ y → first-value (suc n) ↓ y
  done {n} = cong Prelude.[ (λ _ → first-value n) , just ]

  -- If f n terminates with a certain value, then first-value n
  -- terminates with the same value.

  f↓→first-value↓ : ∀ {y} n → f n ↓ y → first-value n ↓ y
  f↓→first-value↓ zero    f↓ = f↓
  f↓→first-value↓ (suc n) f↑ = done f↑

  -- If first-value m terminates with a certain value, then there is
  -- some n for which f n terminates with the same value.

  first-value↓→f↓ : ∀ {y} m → first-value m ↓ y → ∃ λ n → f n ↓ y
  first-value↓→f↓     zero    first-value↓ = zero , first-value↓
  first-value↓→f↓ {y} (suc n) first-value↓ with inspect (f (suc n))
  ... | just y′ , f↓ = suc n , (f (suc n)            ≡⟨ f↓ ⟩
                                just y′              ≡⟨ sym (done f↓) ⟩
                                first-value (suc n)  ≡⟨ first-value↓ ⟩∎
                                just y               ∎)
  ... | nothing , f↑ =
    first-value↓→f↓ n (first-value n        ≡⟨ sym (step f↑) ⟩
                       first-value (suc n)  ≡⟨ first-value↓ ⟩∎
                       just y               ∎)

  -- The function first-value is an increasing sequence.

  inc : Increasing first-value
  inc n with inspect (first-value n) | inspect (f (suc n))
  inc n | _ | nothing , f↑ =
    inj₁ (first-value n        ≡⟨ sym (step f↑) ⟩∎
          first-value (suc n)  ∎)
  inc n | nothing , first-value↑ | just y , f↓ =
    inj₂ (first-value↑ , λ first-value↑ → ⊎.inj₁≢inj₂ (
                             nothing              ≡⟨ sym first-value↑ ⟩
                             first-value (suc n)  ≡⟨ done f↓ ⟩∎
                             just y               ∎))
  inc n | just y , first-value↓ | just y′ , f↓ =
    inj₁ (first-value n        ≡⟨ first-value↓ ⟩
          just y               ≡⟨ cong just $ unique (_ , proj₂ (first-value↓→f↓ n first-value↓)) (_ , f↓) ⟩
          just y′              ≡⟨ sym (done f↓) ⟩∎
          first-value (suc n)  ∎)

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module AnonymousDecl where

_ : Set₁
_ = Set

_ : Set → Set
_ = λ x → x

_∋_ : ∀ {ℓ} (A : Set ℓ) → A → A
A ∋ a = a

_ = Set₁
_ = (Set → Set) ∋ λ x → x

data Bool : Set where t f : Bool

not : Bool → Bool
not t = f
not f = t

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

_ : ∀ x → not (not x) ≡ x
_ = λ { t → refl; f → refl }


text:
open import FRP.JS.Time.Core using ( Time )

module FRP.JS.RSet where

infixr 1 _⇒_

RSet : Set₁
RSet = Time → Set

_⇒_ : RSet → RSet → RSet
(A ⇒ B) t = A t → B t

⟨_⟩ : Set → RSet
⟨ A ⟩ t = A

⟦_⟧ : RSet → Set
⟦ A ⟧ = ∀ {t} → A t

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
-- Andreas, 2016-12-30 test case for #2369

-- {-# OPTIONS --allow-unsolved-metas #-}
-- {-# OPTIONS -v scope.import:20 #-}

module Issue2369 where

import Issue2369.OpenIP

-- Error is:

-- Module cannot be imported since it has open interaction points
-- (consider adding {-# OPTIONS --allow-unsolved-metas #-} to this
-- module)
-- when scope checking the declaration
--   import Issue2369.OpenIP

-- Error could be better, or this could just work.


text:
module <-trans-revisited where

open import Data.Nat using (ℕ; suc)

open import Relations using (_≤_; z≤n; s≤s; ≤-trans; _<_; z<s; s<s)
open import ≤-iff-< using (≤-iff-<′)

<-iff-≤ : ∀ {m n : ℕ}
  → m < n
    ---------
  → suc m ≤ n
<-iff-≤ z<s       = s≤s z≤n
<-iff-≤ (s<s m<n) = s≤s (<-iff-≤ m<n)

-- <-trans の別証明 (≤-trans版)
<-trans-revisited : ∀ {m n p : ℕ}
  → m < n
  → n < p
    -----
  → m < p
<-trans-revisited z<s       (s<s n<p) = ≤-iff-<′ (≤-trans (<-iff-≤ z<s) (<-iff-≤ (s<s n<p)))
<-trans-revisited (s<s m<n) (s<s n<p) = ≤-iff-<′ (≤-trans (s≤s (<-iff-≤ (lemma m<n))) (<-iff-≤ (s<s n<p)))
  where
    lemma : ∀ {m n : ℕ}
      → m < n
        ---------
      → m < suc n
    lemma z<s       = z<s
    lemma (s<s m<n) = s<s (lemma m<n)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
postulate
  A : Set

data B (a : A) : Set where
  conB : B a → B a → B a

data C (a : A) : B a → Set where
  conC : {bl br : B a} → C a bl → C a br → C a (conB bl br)

-- First bug.
{-
a !=<
"An internal error has occurred. Please report this as a bug.\nLocation of the error: src/full/Agda/TypeChecking/Telescope.hs:68\n"
of type A
when checking that the type
(a : A) (b : B a) (tl : C a (_16 a b)) →
C a (_16 a b) → (tr : C a (_17 a b)) → Set
of the generated with function is well-formed
-- Is there a contained error printing bug?
-}
goo : (a : A) (b : B a) (c : C a _) → Set
                                 -- giving b for _ resolves the error
goo a b (conC tl tr) with tl
... | _ = _


text:
------------------------------------------------------------------------
-- Correct-by-construction pretty-printing
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- A pretty-printing library that guarantees that pretty-printers are
-- correct (on the assumption that grammars are unambiguous).

{-# OPTIONS --guardedness #-}

module README where

-- Various utility functions.

import Utilities

-- Infinite grammars.

import Grammar.Infinite.Basic
import Grammar.Infinite

-- Pretty-printing (documents and document combinators).

import Pretty

-- Document renderers.

import Renderer

-- Examples.

import Examples.Bool
import Examples.Expression
import Examples.Identifier
import Examples.Identifier-list
import Examples.Precedence
import Examples.Tree
import Examples.XML

-- Abstract grammars. (Not used by the pretty-printer.)

import Grammar.Abstract

-- Grammars defined as functions from non-terminals to productions.
-- (Not used by the pretty-printer.)

import Grammar.Non-terminal

-- A README directed towards readers of the paper
-- "Correct-by-Construction Pretty-Printing".

import README.Correct-by-Construction-Pretty-Printing

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
{-# OPTIONS --without-K --rewriting #-}

open import HoTT

{- Maybe it is actually easier to prove [sum-subindicator]
   and then derive the other lemma. -}

module groups.SumOfSubIndicator where

module _ {i} (G : Group i) where

  open Group G

  abstract
    sum-ident : ∀ {I} (f : Fin I → El)
      → (∀ <I → f <I == ident)
      → sum f == ident
    sum-ident {I = O} f z = idp
    sum-ident {I = S I} f z =
      ap2 comp
        (sum-ident (f ∘ Fin-S) (z ∘ Fin-S))
        (z (I , ltS))
      ∙ unit-l _

    sum-subindicator : ∀ {I} (f : Fin I → El) <I*
      → (sub-indicator : ∀ {<I} → <I ≠ <I* → f <I == ident)
      → sum f == f <I*
    sum-subindicator f (I , ltS) subind =
      ap (λ g → comp g (f (I , ltS)))
        (sum-ident (f ∘ Fin-S) (λ <I → subind (ltSR≠ltS <I)))
      ∙ unit-l _
    sum-subindicator {I = S I} f (m , ltSR m<I) subind =
      ap2 comp
        (sum-subindicator (f ∘ Fin-S) (m , m<I) (subind ∘ Fin-S-≠))
        (subind (ltS≠ltSR (m , m<I)))
      ∙ unit-r _

module _ {i j k} (G : Group i) {A : Type j} {B : Type k}
  {I} (p : Fin I ≃ Coprod A B) (f : B → Group.El G) b*
  (sub-indicator : ∀ {b} → b ≠ b* → f b == Group.ident G)
  where

  open Group G

  abstract
    private
      sub-indicator' : ∀ {<I} → <I ≠ <– p (inr b*)
        → Coprod-rec (λ _ → ident) f (–> p <I) == ident
      sub-indicator' {<I} <I≠p⁻¹b* =
        Coprod-elim
          {C = λ c → c ≠ inr b* → Coprod-rec (λ _ → ident) f c == ident}
          (λ _ _ → idp)
          (λ b inrb≠inrb* → sub-indicator (inrb≠inrb* ∘ ap inr))
          (–> p <I) (<I≠p⁻¹b* ∘ equiv-adj p)

    subsum-r-subindicator : subsum-r (–> p) f == f b*
    subsum-r-subindicator =
      sum-subindicator G
        (Coprod-rec (λ _ → ident) f ∘ –> p)
        (<– p (inr b*))
        sub-indicator'
      ∙ ap (Coprod-rec (λ _ → ident) f) (<–-inv-r p (inr b*))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Issue502 where

record R : Set where
  record S (A : Set) : Set where
    field
      f : A → A

max_forks_repo_name: Agda-zh/agda


text:
--------------------------------------------------------------------------------
-- This file is the entry point for checking or executing code. It provides the
-- type MetaContext, which tracks the entire state of the interpreter as well as
-- the function tryExecute to parse and execute some code if possible
--------------------------------------------------------------------------------

{-# OPTIONS --type-in-type #-}

module Execution where

open import Class.Monad.Except
open import Class.Monad.IO
open import Class.Monad.State
open import Data.HSTrie

open import Conversion
open import CoreTheory

open import Parse.TreeConvert
open import Parse.Generate

open import Prelude
open import Prelude.Strings

record MetaEnv : Set where
  field
    grammar   : Grammar
    namespace : String  -- we need to remember the current namespace
                        -- because the rule string in the grammar doesn't
    evaluator : AnnTerm

-- The full state of the interpreter: the context of defined values plus parsing
-- and semantics for generating code
MetaContext : Set
MetaContext = GlobalContext × MetaEnv

-- Many statements just return a single string, in which case this function can
-- be used
strResult : String → MetaResult
strResult s = [ s ] , []

getParserNamespace : Context → String → List String
getParserNamespace (Γ , _) n = strDrop (strLength n + 1) <$> (trieKeys $ lookupHSTrie n Γ)

module _ {M : Set → Set} {{_ : Monad M}}
  {{_ : MonadExcept M String}} {{_ : MonadState M MetaContext}} where

  getContext : M Context
  getContext = gets (globalToContext ∘ proj₁)

  getMeta : M MetaEnv
  getMeta = gets proj₂

  modify' : (MetaContext → MetaContext) → M ⊤
  modify' f = modify f >> return tt

  setMeta : MetaEnv → M ⊤
  setMeta menv =
    modify' λ { (Γ , _) → (Γ , menv) }

  setContext : GlobalContext → M ⊤
  setContext Γ = modify' λ { (_ , m) → (Γ , m) }

  modifyContext : (GlobalContext → GlobalContext) → M ⊤
  modifyContext f = do
    Γ ← getContext
    setContext $ f $ contextToGlobal Γ

  addDef : GlobalName → Def → M String
  addDef n d = do
    Γ ← getContext
    case insertInGlobalContext n d (contextToGlobal Γ) of λ where
      (inj₁ x) → throwError x
      (inj₂ y) → setContext y >> return ("Defined " + n + show d)

  unquoteFromTerm : ∀ {A} ⦃ _ : Unquote A ⦄ → PureTerm → M A
  unquoteFromTerm t = do
    Γ ← getContext
    catchError (unquoteConstrs Γ $ normalizePure Γ t)
               (λ e → throwError $ "Error while unquoting" <+> show t + ":\n" + e)

  -- Typecheck a term and return its type
  inferType : AnnTerm → M AnnTerm
  inferType t = do
    Γ ← getContext
    synthType Γ t

  checkType : AnnTerm → AnnTerm → M ⊤
  checkType t T = do
    t' ← inferType t
    inferType T
    Γ ← getContext
    catchError (checkβη Γ T t')
      (λ e → throwError $
        "Type mismatch with the provided type!\n" + e + "\nProvided: " + show t' +
        "\nSynthesized: " + show T)

  checkTypePure : AnnTerm → PureTerm → M ⊤
  checkTypePure t T = do
    t' ← inferType t
    Γ ← getContext
    catchError (checkβηPure Γ T $ Erase t')
      (λ e → throwError $
        "Type mismatch with the provided type!\n" + e + "\nProvided: " + show t' +
        "\nSynthesized: " + show T)

  parseMeta : MetaEnv → String → M (AnnTerm × String)
  parseMeta menv s = let open MetaEnv menv in parse grammar (initNT grammar) namespace s

module ExecutionDefs {M : Set → Set} {{_ : Monad M}}
  {{_ : MonadExcept M String}} {{_ : MonadState M MetaContext}} {{_ : MonadIO M}}
  where

  {-# NON_TERMINATING #-}
  -- Execute a term of type M t for some t
  executeTerm : PureTerm → M (MetaResult × PureTerm)
  executeStmt : Stmt → M MetaResult
  executePrimitive : (m : PrimMeta) → primMetaArgs PureTerm m → M (MetaResult × AnnTerm)
  -- Parse and execute a string
  parseAndExecute' parseAndExecuteBootstrap : String → M (MetaResult × String)
  parseAndExecute : String → M MetaResult

  executeStmt (Let n t nothing) = do
    T ← inferType t
    strResult <$> addDef n (Let t T)

  executeStmt (Let n t (just t')) = do
    checkType t t'
    strResult <$> addDef n (Let t t')

  executeStmt (Ass n t) = do
    _ ← inferType t
    strResult <$> addDef n (Axiom t)

  executeStmt (SetEval t n start) = do
    Γ ← getContext
    y ← generateCFG start $ getParserNamespace Γ n
    (Pi-A _ u u₁) ← hnfNorm Γ <$> synthType Γ t
      where _ → throwError "The evaluator needs to have a pi type"
    appendIfError (checkβη Γ u $ FreeVar (n + "$" + start))
      "The evaluator needs to accept the parse result as input"
    case (hnfNorm Γ u₁) of λ where
      (M-A _) → do
        setMeta record { grammar = y ; namespace = n ; evaluator = t }
        return $ strResult "Successfully set the evaluator"
      _       → throwError "The evaluator needs to return a M type"

  executeStmt (Import x) = do
    res ← liftIO $ readFiniteFileError (x + ".mced")
    case res of λ where
      (inj₁ x) → throwError x
      (inj₂ y) → parseAndExecute y

  executeStmt Empty = return (strResult "")

  executeTerm (Mu-P t t₁) = do
    Γ ← getContext
    (res , t') ← executeTerm (hnfNormPure Γ t)
    (res' , resTerm) ← executeTerm (hnfNormPure Γ (t₁ ⟪$⟫ t'))
    return (res + res' , resTerm)

  executeTerm (Epsilon-P t) = return (([] , []) , t)

  executeTerm (Gamma-P t t') =
    catchError (executeTerm t) (λ s → executeTerm (t' ⟪$⟫ quoteToPureTerm s))

  executeTerm (Ev-P m t) = do
    (res , t') ← executePrimitive m t
    checkTypePure t' $ primMetaT m t
    return (res , Erase t')

  {-# CATCHALL #-}
  executeTerm t =
    throwError ("Error: " + show t + " is not a term that can be evaluated!")

  executePrimitive EvalStmt t = do
    Γ ← getContext
    stmt ← unquoteFromTerm t
    res ← executeStmt stmt
    return (res , quoteToAnnTerm res)

  executePrimitive ShellCmd (t , t') = do
    Γ ← getContext
    cmd ← unquoteFromTerm t
    args ← unquoteFromTerm t'
    res ← liftIO $ runShellCmd cmd args
    return (strResult res , quoteToAnnTerm res)

  executePrimitive CheckTerm (t , t') = do
    Γ ← getContext
    u ← unquoteFromTerm t'
    T' ← inferType u
    catchError (checkβηPure Γ t $ Erase T')
      (λ e → throwError $
        "Type mismatch with the provided type!\nProvided: " + show t +
        "\nSynthesized: " + show T')
    return (strResult "" , u)

  executePrimitive Parse (t , type , t') = do
    Γ ← getContext
    nonTerminal ← M String ∋ (unquoteFromTerm t)
    text ← M String ∋ (unquoteFromTerm t')
    record { grammar = G ; namespace = namespace } ← getMeta
    NT ← maybeToError (findNT G nonTerminal)
                      ("Non-terminal" <+> nonTerminal <+> "does not exist in the current grammar!")
    (res , rest) ← parse G NT namespace text
    T ← appendIfError (synthType Γ res)
                      ("\n\nError while interpreting input: "
                        + (shortenString 10000 (show res))
                        + "\nWhile parsing: " + (shortenString 10000 text))
    appendIfError (checkβηPure Γ type $ Erase T)
      ("Type mismatch with the provided type!\nProvided: " + show type +
        "\nSynthesized: " + show T)
    -- need to spell out instance manually, since we don't want to quote 'res'
    return (strResult "" , quoteToAnnTerm ⦃ Quotable-ProductData ⦃ Quotable-NoQuoteAnnTerm ⦄ ⦄
      record { lType = T ; rType = FreeVar "init$string" ; l = res ; r = rest })

  executePrimitive Normalize t = do
    Γ ← getContext
    u ← unquoteFromTerm t
    T ← synthType Γ u
    return (strResult
      (show u + " : " + show T + " normalizes to: " +
      (show $ normalizePure Γ $ Erase u)) , (quoteToAnnTerm $ normalizePure Γ $ Erase u))

  executePrimitive HeadNormalize t = do
    Γ ← getContext
    u ← unquoteFromTerm t
    T ← synthType Γ u
    return (strResult
      (show t + " : " + show T + " head-normalizes to: " +
      (show $ hnfNorm Γ u)) , (quoteToAnnTerm $ hnfNorm Γ u))

  executePrimitive InferType t = do
    Γ ← getContext
    u ← unquoteFromTerm t
    T ← synthType Γ u
    return (strResult "" , (quoteToAnnTerm T))

  parseAndExecuteBootstrap s = do
    (fst , snd) ← parseStmt s
    res ← appendIfError (executeStmt fst) ("\n\nError while executing statement: " + show fst)
    return (res , snd)

  parseAndExecute' s = do
    Γ ← getContext
    m ← getMeta
    (fst , snd) ← parseMeta m s
    let exec = MetaEnv.evaluator m ⟪$⟫ fst
    (M-A _) ← hnfNorm Γ <$>
      appendIfError (synthType Γ exec)
                    ("\n\nError while interpreting input: "
                      + (shortenString 10000 (show fst))
                      + "\nWhile parsing: " + (shortenString 10000 s))
      where _ → throwError "Trying to execute something that isn't of type M t. This should never happen!"
    let execHnf = hnfNormPure Γ $ Erase exec
    (res , _) ← appendIfError (executeTerm execHnf) ("\n\nError while executing input: " + s)
    return (res , snd)

  parseAndExecute s = do
    record { evaluator = evaluator } ← getMeta
    (res , rest) ← case evaluator of λ where
      (Sort-A □) → parseAndExecuteBootstrap s
      _          → parseAndExecute' s
    res' ← if strNull rest then return mzero else parseAndExecute rest
    return (res + res')

module ExecutionMonad where
  open import Monads.ExceptT
  open import Monads.StateT

  ExecutionState : Set
  ExecutionState = MetaContext

  contextFromState : ExecutionState → MetaContext
  contextFromState s = s

  Execution : Set → Set
  Execution = ExceptT (StateT IO ExecutionState) String

  execute : ∀ {A} → Execution A → MetaContext → IO (ExecutionState × (String ⊎ A))
  execute x Γ = do
    (x' , s') ← x Γ
    return (s' , x')

  instance
    Execution-Monad : Monad Execution
    Execution-Monad = ExceptT-Monad {{StateT-Monad}}

    Execution-MonadExcept : MonadExcept Execution {{Execution-Monad}} String
    Execution-MonadExcept = ExceptT-MonadExcept {{StateT-Monad}}

    Execution-MonadState : MonadState Execution {{Execution-Monad}} ExecutionState
    Execution-MonadState = ExceptT-MonadState {{StateT-Monad}} {{StateT-MonadState}}

    Execution-IO : MonadIO Execution {{Execution-Monad}}
    Execution-IO = ExceptT-MonadIO {{StateT-Monad}} {{StateT-MonadIO {{_}} {{IO-MonadIO}}}}

open ExecutionMonad public
open ExecutionDefs {Execution} public

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
{-# OPTIONS --erased-cubical --safe #-}

module Instruments where

open import Data.Fin  using (#_)
open import MidiEvent using (InstrumentNumber-1; maxChannels)
open import Data.Vec        using (Vec; []; _∷_)

-- Start of an instrument list

-- all instruments have this type
piano : InstrumentNumber-1

piano                 = # 0
brightPiano           = # 1
electricGrandPiano    = # 2
honkyTonkPiano        = # 3
electricPiano1        = # 4
electricPiano2        = # 5
harpsichord           = # 6
clavinet              = # 7

celesta               = # 8
vibraphone            = # 11

drawbarOrgan          = # 16
percussiveOrgan       = # 17
rockOrgan             = # 18
churchOrgan           = # 19

acousticGuitar[nylon] = # 24
acousticGuitar[steel] = # 25
electricGuitar[jazz]  = # 26
electricGuitar[clean] = # 27
electricGuitar[muted] = # 28
overdrivenGuitar      = # 29
distortionGuitar      = # 30
guitarHarmonics       = # 31

harp                  = # 46

----------------

drums : InstrumentNumber-1
drums      = # 0

----------------

-- Assign piano to all tracks
-- Note that channel 10 (9 as Channel-1) is percussion
pianos : Vec InstrumentNumber-1 maxChannels
pianos =
  piano ∷ -- 1
  piano ∷ -- 2
  piano ∷ -- 3
  piano ∷ -- 4
  piano ∷ -- 5
  piano ∷ -- 6
  piano ∷ -- 7
  piano ∷ -- 8
  piano ∷ -- 9
  drums ∷ -- 10 (percussion)
  piano ∷ -- 11
  piano ∷ -- 12
  piano ∷ -- 13
  piano ∷ -- 14
  piano ∷ -- 15
  piano ∷ -- 16
  []

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Documentation for the List type
------------------------------------------------------------------------

{-# OPTIONS --warning noMissingDefinitions #-}

module README.Data.List where

open import Algebra.Structures using (IsCommutativeMonoid)
open import Data.Char.Base using (Char; fromℕ)
open import Data.Char.Properties as CharProp hiding (setoid)
open import Data.Nat using (ℕ; _+_; _<_; s≤s; z≤n; _*_; _∸_; _≤_)
open import Data.Nat.Properties as NatProp
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; cong; setoid)

------------------------------------------------------------------------
-- 1. Basics
------------------------------------------------------------------------
-- The `List` datatype is exported by the following file:

open import Data.List
  using
  (List
  ; []; _∷_
  ; sum; map; take; reverse; _++_; drop
  )

module Basics where

  -- Lists are built using the "[]" and "_∷_" constructors.

  list₁ : List ℕ
  list₁ = 3 ∷ 1 ∷ 2 ∷ []

  -- Basic operations over lists are also exported by the same file.

  lem₁ : sum list₁ ≡ 6
  lem₁ = refl

  lem₂ : map (_+ 2) list₁ ≡ 5 ∷ 3 ∷ 4 ∷ []
  lem₂ = refl

  lem₃ : take 2 list₁ ≡ 3 ∷ 1 ∷ []
  lem₃ = refl

  lem₄ : reverse list₁ ≡ 2 ∷ 1 ∷ 3 ∷ []
  lem₄ = refl

  lem₅ : list₁ ++ list₁ ≡ 3 ∷ 1 ∷ 2 ∷ 3 ∷ 1 ∷ 2 ∷ []
  lem₅ = refl

  -- Various properties of these operations can be found in:

  open import Data.List.Properties

  lem₆ : ∀ n (xs : List ℕ) → take n xs ++ drop n xs ≡ xs
  lem₆ = take++drop

  lem₇ : ∀ (xs : List ℕ) → reverse (reverse xs) ≡ xs
  lem₇ = reverse-involutive

  lem₈ : ∀ (xs ys zs : List ℕ) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
  lem₈ = ++-assoc

------------------------------------------------------------------------
-- 2. Binary relations over lists
------------------------------------------------------------------------

-- All binary relations over lists are found in the folder
-- `Data.List.Relation.Binary`.

------------------------------------------------------------------------
-- Pointwise

module PointwiseExplanation where

  -- One of the most basic ways to form a binary relation between two
  -- lists of type `List A`, given a binary relation over `A`, is to say
  -- that two lists are related if:
  --   i) the first elements in the lists are related
  --   ii) the second elements in the lists are related
  --   iii) the third elements in the lists are related etc.
  --
  -- A formalisation of this "pointwise" lifting of a relation to lists
  -- is found in:

  open import Data.List.Relation.Binary.Pointwise

  -- The same syntax to construct a list (`[]` & `_∷_`) is used to
  -- construct proofs for the `Pointwise` relation. For example if you
  -- want to prove that one list is strictly less than another list:

  lem₁ : Pointwise _<_ (0 ∷ 2 ∷ 1 ∷ []) (1 ∷ 4 ∷ 2 ∷ [])
  lem₁ = 0<1 ∷ 2<4 ∷ 1<2 ∷ []
    where
    0<1 = s≤s z≤n
    2<4 = s≤s (s≤s (s≤s z≤n))
    1<2 = s≤s 0<1

  -- Lists that are related by `Pointwise` must be of the same length.
  -- For example:

  open import Relation.Nullary using (¬_)

  lem₂ : ¬ Pointwise _<_ (0 ∷ 2 ∷ []) (1 ∷ [])
  lem₂ (0<1 ∷ ())

------------------------------------------------------------------------
-- Equality

module EqualityExplanation where

  -- There are many different options for what it means for two
  -- different lists of type `List A` to be "equal". We will initially
  -- consider notions of equality that require the list elements to be
  -- in the same order and later discuss other types of equality.

  -- The most basic option in the former case is simply to use
  -- propositional equality `_≡_` over lists:

  open import Relation.Binary.PropositionalEquality
    using (_≡_; sym; refl)

  lem₁ : 1 ∷ 2 ∷ 3 ∷ [] ≡ 1 ∷ 2 ∷ 3 ∷ []
  lem₁ = refl

  -- However propositional equality is only suitable when we want to
  -- use propositional equality to compare the individual elements.
  -- Although a contrived example, consider trying to prove the
  -- equality of two lists of the type `List (ℕ → ℕ)`:

  lem₂ : (λ x → 2 * x + 2) ∷ [] ≡ (λ x → 2 * (x + 1)) ∷ []

  -- In such a case it is impossible to prove the two lists equal with
  -- refl as the two functions are not propositionally equal. In the
  -- absence of postulating function extensionality (see README.Axioms),
  -- the most common definition of function equality is to say that two
  -- functions are equal if their outputs are always propositionally
  -- equal for any input. This notion of function equality `_≗_` is
  -- found in:

  open import Relation.Binary.PropositionalEquality using (_≗_)

  -- We now want to use the `Pointwise` relation to say that the two
  -- lists are equal if their elements are pointwise equal with resepct
  -- to `_≗_`. However instead of using the pointwise module directly
  -- to write:

  open import Data.List.Relation.Binary.Pointwise using (Pointwise)

  lem₃ : Pointwise _≗_ ((λ x → x + 1) ∷ []) ((λ x → x + 2 ∸ 1) ∷ [])

  -- the library provides some nicer wrappers and infix notation in the
  -- folder "Data.List.Relation.Binary.Equality".

  -- Within this folder there are four different modules.

  import Data.List.Relation.Binary.Equality.Setoid           as SetoidEq
  import Data.List.Relation.Binary.Equality.DecSetoid        as DecSetoidEq
  import Data.List.Relation.Binary.Equality.Propositional    as PropEq
  import Data.List.Relation.Binary.Equality.DecPropositional as DecPropEq

  -- Which one should be used depends on whether the underlying equality
  -- over "A" is:
  --   i)  propositional or setoid-based
  --   ii) decidable.

  -- Each of the modules except `PropEq` are designed to be opened with a
  -- module parameter. This is to avoid having to specify the underlying
  -- equality relation or the decidability proofs every time you use the
  -- list equality.

  -- In our example function equality is not decidable and not propositional
  -- and so we want to use the `SetoidEq` module. This requires a proof that
  -- the `_≗_` relation forms a setoid over functions of the type `ℕ → ℕ`.
  -- This is found in:

  open import Relation.Binary.PropositionalEquality using (_→-setoid_)

  -- The `SetoidEq` module should therefore be opened as follows:

  open SetoidEq (ℕ →-setoid ℕ)

  -- All four equality modules provide an infix operator `_≋_` for the
  -- new equality relation over lists. The type of `lem₃` can therefore
  -- be rewritten as:

  lem₄ : (λ x → x + 1) ∷ [] ≋ (λ x → x + 2 ∸ 1) ∷ []
  lem₄ = 2x+2≗2[x+1] ∷ []
    where
    2x+2≗2[x+1] : (λ x → x + 1) ≗ (λ x → x + 2 ∸ 1)
    2x+2≗2[x+1] x = sym (+-∸-assoc x (s≤s z≤n))

  -- The modules also provide proofs that the `_≋_` relation is a
  -- setoid in its own right and therefore is reflexive, symmetric,
  -- transitive:

  lem₅ : (λ x → 2 * x + 2) ∷ [] ≋ (λ x → 2 * x + 2) ∷ []
  lem₅ = ≋-refl

  -- If we could prove that `_≗_` forms a `DecSetoid` then we could use
  -- the module `DecSetoidEq` instead. This exports everything from
  -- `SetoidEq` as well as the additional proof `_≋?_` that the list
  -- equality is decidable.

  -- This pattern of four modules for each of the four different types
  -- of equality is repeated throughout the library (e.g. see the
  -- `Membership` subheading below). Note that in this case the modules
  -- `PropEq` and `DecPropEq` are not very useful as if two lists are
  -- pointwise propositionally equal they are necessarily
  -- propositionally equal (and vice-versa). There are proofs of this
  -- fact exported by `PropEq` and `DecPropEq`. Although, these two
  -- types of list equality are not very useful in practice, they are
  -- included for completeness's sake.

------------------------------------------------------------------------
-- Permutations

module PermutationExplanation where

  -- Alternatively you might consider two lists to be equal if they
  -- contain the same elements regardless of the order of the elements.
  -- This is known as either "set equality" or a "permutation".

  -- The easiest-to-use formalisation of this relation is found in the
  -- module:

  open import Data.List.Relation.Binary.Permutation.Propositional

  -- The permutation relation is written as `_↭_` and has four
  -- constructors. The first `refl` says that a list is always
  -- a permutation of itself, the second `prep` says that if the
  -- heads of the lists are the same they can be skipped, the third
  -- `swap` says that the first two elements of the lists can be
  -- swapped and the fourth `trans` says that permutation proofs
  -- can be chained transitively.

  -- For example a proof that two lists are a permutation of one
  -- another can be written as follows:

  lem₁ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ []
  lem₁ = trans (prep 1 (swap 2 3 refl)) (swap 1 3 refl)

  -- In practice it is difficult to parse the constructors in the
  -- proof above and hence understand why it holds. The
  -- `PermutationReasoning` module can be used to write this proof
  -- in a much more readable form:

  open PermutationReasoning

  lem₂ : 1 ∷ 2 ∷ 3 ∷ [] ↭ 3 ∷ 1 ∷ 2 ∷ []
  lem₂ = begin
    1 ∷ 2 ∷ 3 ∷ []  ↭⟨ prep 1 (swap 2 3 refl) ⟩
    1 ∷ 3 ∷ 2 ∷ []  ↭⟨ swap 1 3 refl ⟩
    3 ∷ 1 ∷ 2 ∷ []  ∎

  -- As might be expected, properties of the permutation relation may be
  -- found in `Data.List.Relation.Binary.Permutation.Inductive.Properties`.

  open import Data.List.Relation.Binary.Permutation.Propositional.Properties

  lem₃ : ∀ {xs ys : List ℕ} → xs ↭ ys → map fromℕ xs ↭ map fromℕ ys
  lem₃ = map⁺ fromℕ

  lem₄ : IsCommutativeMonoid {A = List ℕ} _↭_ _++_ []
  lem₄ = ++-isCommutativeMonoid

  -- Note: at the moment permutations have only been formalised for
  -- propositional equality. Permutations for the other three types of
  -- equality (decidable propositional, setoid and decidable setoid)
  -- will hopefully be added in later versions of the library.

------------------------------------------------------------------------
-- Other relations

-- There exist many other binary relations in the
-- `Data.List.Relation.Binary` folder, including:
--    1. lexicographic orderings
--    2. bag/multiset equality
--    3. the subset relations.
--    4. the sublist relations

------------------------------------------------------------------------
-- 3. Properties of lists
------------------------------------------------------------------------

-- Whereas binary relations deal with how two lists relate to one
-- another, the unary relations in `Data.List.Relation.Unary` are used
-- to reason about the properties of an individual list.

------------------------------------------------------------------------
-- Any

module AnyExplanation where

  -- The predicate `Any` encodes the idea of at least one element of a
  -- given list satisfying a given property (or more formally a
  -- predicate, see the `Pred` type in `Relation.Unary`).

  open import Data.List.Relation.Unary.Any as Any

  -- A proof of type Any consists of a sequence of the "there"
  -- constructors, which says that the element lies in the remainder of
  -- the list, followed by a single "here" constructor which indicates
  -- that the head of the list satisfies the predicate and takes a proof
  -- that it does so.

  -- For example a proof that a given list of natural numbers contains
  -- at least one number greater than or equal to 4 can be written as
  -- follows:

  lem₁ : Any (4 ≤_) (3 ∷ 5 ∷ 1 ∷ 6 ∷ [])
  lem₁ = there (here 4≤5)
    where
    4≤5 = s≤s (s≤s (s≤s (s≤s z≤n)))

  -- Note that nothing requires that the proof of `Any` points at the
  -- first such element in the list. There is therefore an alternative
  -- proof for the above lemma which points to 6 instead of 5.

  lem₂ : Any (4 ≤_) (3 ∷ 5 ∷ 1 ∷ 6 ∷ [])
  lem₂ = there (there (there (here 4≤6)))
    where
    4≤6 = s≤s (s≤s (s≤s (s≤s z≤n)))

  -- There also exist various operations over proofs of `Any` whose names
  -- shadow the corresponding list operation. The standard way of using
  -- these is to use `as` to name the module:

  import Data.List.Relation.Unary.Any as Any

  -- and then use the qualified name `Any.map`. For example, map can
  -- be used to change the predicate of `Any`:

  open import Data.Nat.Properties using (≤-trans; n≤1+n)

  lem₃ : Any (3 ≤_) (3 ∷ 5 ∷ 1 ∷ 6 ∷ [])
  lem₃ = Any.map 4≤x⇒3≤x lem₂
    where
    4≤x⇒3≤x : ∀ {x} → 4 ≤ x → 3 ≤ x
    4≤x⇒3≤x = ≤-trans (n≤1+n 3)

------------------------------------------------------------------------
-- All

module AllExplanation where

  -- The dual to `Any` is the predicate `All` which encodes the idea that
  -- every element in a given list satisfies a given property.

  open import Data.List.Relation.Unary.All

  -- Proofs for `All` are constructed using exactly the same syntax as
  -- is used to construct lists ("[]" & "_∷_"). For example to prove
  -- that every element in a list is less than or equal to one:

  lem₁ : All (_≤ 1) (1 ∷ 0 ∷ 1 ∷ [])
  lem₁ = 1≤1 ∷ 0≤1 ∷ 1≤1 ∷ []
    where
    0≤1 = z≤n
    1≤1 = s≤s z≤n

  -- As with `Any`, the module also provides the standard operators
  -- `map`, `zip` etc. to manipulate proofs for `All`.

  import Data.List.Relation.Unary.All as All
  open import Data.Nat.Properties using (≤-trans; n≤1+n)

  lem₂ : All (_≤ 2) (1 ∷ 0 ∷ 1 ∷ [])
  lem₂ = All.map ≤1⇒≤2 lem₁
    where
    ≤1⇒≤2 : ∀ {x} → x ≤ 1 → x ≤ 2
    ≤1⇒≤2 x≤1 = ≤-trans x≤1 (n≤1+n 1)

------------------------------------------------------------------------
-- Membership

module MembershipExplanation where

  -- Membership of a list is simply a special case of `Any` where
  -- `x ∈ xs` is defined as `Any (x ≈_) xs`.

  -- Just like pointwise equality of lists, the exact membership module
  -- that should be used depends on whether the equality on the
  -- underlying elements of the list is i) propositional or setoid-based
  -- and ii) decidable.

  import Data.List.Membership.Setoid as SetoidMembership
  import Data.List.Membership.DecSetoid as DecSetoidMembership
  import Data.List.Membership.Propositional as PropMembership
  import Data.List.Membership.DecPropositional as DecPropMembership

  -- For example if we want to reason about membership for `List ℕ`
  -- then you would use the `DecSetoidMembership` as we use
  -- propositional equality over `ℕ` and it is also decidable. Therefore
  -- the module `DecPropMembership` should be opened as follows:

  open DecPropMembership NatProp._≟_

  -- As membership is just an instance of `Any` we also need to import
  -- the constructors `here` and `there`. (See issue #553 on Github for
  -- why we're struggling to have `here` and `there` automatically
  -- re-exported by the membership modules).

  open import Data.List.Relation.Unary.Any using (here; there)

  -- These modules provide the infix notation `_∈_` which can be used
  -- as follows:

  lem₁ : 1 ∈ 2 ∷ 1 ∷ 3 ∷ []
  lem₁ = there (here refl)

  -- Properties of the membership relation can be found in the following
  -- two files:

  import Data.List.Membership.Setoid.Properties as SetoidProperties
  import Data.List.Membership.Propositional.Properties as PropProperties

  -- As of yet there are no corresponding files for properties of
  -- membership for decidable versions of setoid and propositional
  -- equality as we have no properties that only hold when equality is
  -- decidable.

  -- These `Properties` modules are NOT parameterised in the same way as
  -- the main membership modules as some of the properties relate
  -- membership proofs for lists of different types. For example in the
  -- following the first `∈` refers to lists of type `List ℕ` whereas
  -- the second `∈` refers to lists of type `List Char`.

  open DecPropMembership CharProp._≟_ renaming (_∈_ to _∈ᶜ_)
  open SetoidProperties using (∈-map⁺)

  lem₂ : {v : ℕ} {xs : List ℕ} → v ∈ xs → fromℕ v ∈ᶜ map fromℕ xs
  lem₂ = ∈-map⁺ (setoid ℕ) (setoid Char) (cong fromℕ)


text:
-- {-# OPTIONS -v scope.let:10 #-}

module Issue381 (A : Set) where

data _≡_ (x : A) : A → Set where
  refl : x ≡ x

id : A → A
id x = let abstract y = x in y
-- abstract in let should be disallowed

lemma : ∀ x → id x ≡ x
lemma x = refl

max_issues_repo_name: masondesu/agda


text:
module Metalogic.Classical.Propositional.Syntax {ℓₚ} (Proposition : Set(ℓₚ)) where

import Lvl

infixl 1011 •_
infixl 1010 ¬_
infixl 1005 _∧_
infixl 1004 _∨_
infixl 1000 _⇐_ _⇔_ _⇒_

data Formula : Set(ℓₚ) where
  •_ : Proposition → Formula

  ⊤ : Formula
  ⊥ : Formula

  ¬_ : Formula → Formula

  _∧_ : Formula → Formula → Formula
  _∨_ : Formula → Formula → Formula
  _⇒_ : Formula → Formula → Formula

_⇐_ : Formula → Formula → Formula
_⇐_ a b = _⇒_ b a

_⇔_ : Formula → Formula → Formula
_⇔_ a b = (_⇐_ a b) ∧ (_⇒_ a b)


text:
{-# OPTIONS --cubical --safe #-}

module Lens where

open import Lens.Definition public
open import Lens.Operators public
open import Lens.Composition public
open import Lens.Pair public

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Data.Unit.Instance where

open import Class.Monoid
open import Data.Unit.Polymorphic

instance
  Unit-Monoid : ∀ {a} → Monoid {a} ⊤
  Unit-Monoid = record { mzero = tt ; _+_ = λ _ _ -> tt }