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,

clayrat

From Coq Require Import Program.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype seq ssrnat.
Export Unset Program Cases.
#[local] Obligation Tactic := auto.

Section HoareState.
  Variable S : Type.

  Definition Pre : Type := S -> Prop.
  Definition Post (A : Type) : Type := S -> A -> S -> Prop.

clayrat

{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

module Avl_ext where

import qualified Prelude

#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#if __GLASGOW_HASKELL__ >= 900

clayrat

From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma map_foldr {T1 T2} (f : T1 -> T2) xs :
  map f xs = foldr (fun x ys => f x :: ys) [::] xs.
Proof. by []. Qed.