laMudri

module Classical where

open import Function using (_∘_; case_of_; id; _$_; _∋_)
open import Data.Product using (_×_; _,_; ∃; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Bool
  using (Bool; true; false; not; if_then_else_; T)
  renaming (_∨_ to _b∨_; _∧_ to _b∧_)

laMudri

module Collatz where

open import Coinduction
open import Data.Colist using (Colist; []; _∷_; take)
open import Data.Nat using (ℕ; zero; suc; _*_)
open import Data.Nat.Divisibility using (divides; _∣?_)
open import Data.Nat.Properties using (strictTotalOrder)
open import Function
open import Relation.Binary using (DecSetoid; StrictTotalOrder)
open import Relation.Nullary using (Dec; yes; no)

laMudri

module BySym where

open import Data.List
open import Data.Sum as ⊎
open import Relation.Binary.PropositionalEquality

module _ {a} {A : Set a} where
  infix 4 _≤_
  data _≤_ : (xs ys : List A) → Set where
    []≤[] : [] ≤ []

laMudri

dot : ∀ {γ} (Γ Γ′ : Context γ) → Mult
dot ∅ ∅ = 0#
dot (Γ , π ∙ _) (Γ′ , π′ ∙ _) = dot Γ Γ′ + (π * π′)

-- Induction on the size of the output
-- (filling in each item of the output vector)
_⊛′_ : ∀ {γ δ}
  → (Δ : ∀ {B} → δ ∋ B → Context γ)
  → (Γ : Context γ)
  → Context δ

laMudri

data _⊆_ : ∀ {m m′ n} → m ≤ n → m′ ≤ n → Set where
  ozz : oz ⊆ oz
  oss : ∀ {m m′ n} {th : m ≤ n} {ph : m′ ≤ n} → th ⊆ ph → os th ⊆ os ph
  o′′ : ∀ {m m′ n} {th : m ≤ n} {ph : m′ ≤ n} → th ⊆ ph → o′ th ⊆ o′ ph
  o′s : ∀ {m m′ n} {th : m ≤ n} {ph : m′ ≤ n} → th ⊆ ph → o′ th ⊆ os ph

laMudri

The generic syntax with binding paper [Allais et al, 2018] is sure to keep
contexts parametric throughout all typing rules. It does this by writing only
context *extensions* (where a new variable is bound), and then taking var to be
a special rule. This helps substitution to go through nicely.

When we do anything substructural, it seems that we have to give up this
property. For example, take the intuitionistic MALL natural deduction rule for
tensor introduction.

Γ ⊢ A   Δ ⊢ B

laMudri

-----------------     -----------------
1 v : R² ⊢ v : R²     1 v : R² ⊢ v : R²
------------------    ------------------
1 v : R² ⊢ v.x : R    1 v : R² ⊢ v.y : R
-------------------   -------------------
2 v : R² ⊢ v.x² : R   2 v : R² ⊢ v.y² : R
-----------------------------------------
       2 v : R² ⊢ v.x² + v.y² : R
      -----------------------------
      1 v : R² ⊢ √(v.x² + v.y²) : R

laMudri

{ stdenv, fetchFromGitHub
, autoreconfHook, docbook2x, pkgconfig
, gtk3, dconf, gobject-introspection
, ibus, python3, wrapGAppsHook }:

stdenv.mkDerivation rec {
  name = "ibus-table-${version}";
  version = "1.9.21";

  src = fetchFromGitHub {

laMudri

{-# OPTIONS --cubical #-}
module Diaconescu where

  open import Data.Bool using (true; false)
  open import Data.Empty
  open import Data.Product using (Σ; Σ-syntax; _,_; proj₁; proj₂)
  open import Data.Unit
  open import Level renaming (zero to lzero; suc to lsuc)
  open import Relation.Binary.PropositionalEquality as ≡p
    using (inspect)

laMudri

data Bracket = Open | Close
data Nat = Ze | Su Nat

isZero :: Nat -> Bool
isZero Ze = True
isZero (Su _) = False

match :: [Bracket] -> Bool
match = go Ze
  where