laMudri

{-# OPTIONS --cubical #-}

module Scratch where

open import Cubical.Foundations.Everything
open import Cubical.Data.Equality

module _ {a} {A : Type a} where

  data View {x : A} : {y : A} → x ≡ y → Type a where

laMudri

module Interleaving where

open import Data.List using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise as Pw
open import Data.List.Relation.Ternary.Interleaving.Propositional
open import Data.Product
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
open import Relation.Unary renaming (U to Un)

module _ {a} {A : Set a} where

laMudri

{-# OPTIONS --without-K --postfix-projections --safe #-}
module DiffSolver where

open import Algebra
open import Function.Base
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

module WithMonoid {c ℓ} (monoid : Monoid c ℓ) where
  open Monoid monoid
  open import Relation.Binary.Reasoning.Setoid setoid

laMudri

{-# OPTIONS --cubical --safe --postfix-projections #-}

module Nominal where

  open import Cubical.Foundations.Everything
    renaming (isOfHLevel to IsOfHLevel; isProp to IsProp)
    hiding (_∘_)
  open import Cubical.HITs.PropositionalTruncation
  open import Data.Nat hiding (_⊔_)
  open import Function.Base

laMudri

{-# OPTIONS --safe --without-K --postfix-projections #-}

module NamedDeBruijn where

  open import Data.Bool
  open import Data.Product
  open import Function.Base using (id)
  open import Relation.Binary using (DecidableEquality)
  open import Relation.Binary.PropositionalEquality
  open import Relation.Nullary

laMudri

module(quant).

% Database (algebra)

%! type ann := zero | one | omega.

%! zero(+X:ann) is semidet.
%! add(-X:ann, -Y:ann, +Z:ann) is nondet.
%! one(+X:ann) is semidet.
%! mult(+X:ann, -Y:ann, +Z:ann) is nondet.

laMudri

In Agda, I can write many different records with a lookup field.

record DVec (n : ℕ) (A : Fin n → Set) : Set where
  constructor tabulate
  field lookup : (i : Fin n) → A i
open DVec public

record DMat (m n : ℕ) (A : Fin m → Fin n → Set) : Set where
 constructor tabulate

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

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

{ 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 {