clayrat

open import Prelude
open import Data.Empty
open import Data.Bool renaming (elim to elimᵇ ; rec to recᵇ)
open import Data.Maybe
open import Data.List
open import Data.List.Operations.Discrete
open import Data.List.Correspondences.Unary.All
open import Data.List.Correspondences.Unary.Has
open import Data.List.Correspondences.Unary.Related
open import Data.List.Correspondences.Binary.Perm

clayrat

module Div3DFA where

open import Prelude
open import Data.Bool
open import Data.Nat
open import Data.Nat.Order.Base
open import Data.Nat.DivMod
open import Data.Nat.DivMod.Base
open import Data.List
open import Data.Reflects

clayrat

{-# OPTIONS --safe #-}
module Order.SupLattice.Powerset where

open import Categories.Prelude
open import Meta.Prelude
open import Foundations.Equiv.Size

open import Data.Empty
open import Data.Unit
open import Data.Sum

clayrat

module DepPrism where

open import Prelude

open import Data.Empty
open import Data.Sum

private variable
  ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
  X : 𝒰 ℓ₁

clayrat

{-# OPTIONS --safe --backtracking-instance-search #-}
module Bag where

open import Prelude
open import Data.Nat.Base
open import Data.Fin.Computational.Base
open import Data.Fin.Computational.Instances.Finite
open import Structures.FinSet
open import Bij

clayrat

CoInductive stream (A : Type) : Type :=
| Cons : A
         -> stream A
         -> stream A.

CoInductive infiniteDecreasingChain A (R : A -> A -> Prop) : stream A -> Prop :=
| ChainCons : forall x y s, infiniteDecreasingChain A R (Cons A y s)
                            -> R y x
                            -> infiniteDecreasingChain A R (Cons A x (Cons A y s)).

clayrat

data Bush n l b = Bsh (l -> b) (n -> Bush n l (Bush n l b))

-- polymorphic recursion
mapb :: (b -> c) -> Bush n l b -> Bush n l c
mapb f (Bsh g k) = Bsh (f . g) (\a -> mapb (mapb f) (k a))

data BT n l = L l | Sp (BT n l) n (BT n l)

lamBT :: (BT n l -> b) -> Bush n l b
lamBT f = Bsh (f . L) (\a -> lamBT (\t -> lamBT (\u -> f (Sp t a u))))

clayrat

{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Even where

open import Prelude
open import Data.Unit
open import Data.Empty
open import Data.Bool
open import Data.Nat
open import Data.Nat.Order.Inductive

clayrat

{-# OPTIONS --safe #-}
module qh where

-- https://www.cs.nott.ac.uk/~pszgmh/quotient-haskell.pdf

open import Prelude
open import Meta.Prelude

open import Data.Bool
open import Data.Empty

clayrat

From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype.
From pcm Require Import options axioms prelude pred.
From pcm Require Import pcm unionmap heap.
From htt Require Import options interlude model heapauto.

(* counter that hides local state with an abstract predicate *)

Record cnt : Type :=
  Counter {inv : nat -> Pred heap;
           method : {v : nat}, STsep (inv v,