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 Data.Bool
open import Data.Empty
open import Data.Nat
open import Data.List

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.

clayrat

From Coq Require Import ssreflect ssrbool ssrfun Logic.FunctionalExtensionality.
From mathcomp Require Import ssrnat.

Definition surjection {X Y : Type} (f : X -> Y) :=
  forall y, exists x, f x = y.

Theorem nat_endomorphisms_are_uncountable :
  ~ exists (f : nat -> (nat -> nat)), surjection f.
Proof.
case=>f Hf.

clayrat

(* https://coq.discourse.group/t/indefinite-description-axiom-could-be-simpler/1764 *)
 
From Coq Require Import ssreflect ssrbool ssrfun.

Definition indefinite_description :=
  forall (A : Type) (P : A->Prop), ex P -> sig P.

Definition simple_description :=
  forall (A : Type), inhabited A -> A.

clayrat

-- https://mathoverflow.net/questions/272982/how-do-we-construct-the-g%C3%B6del-s-sentence-in-martin-l%C3%B6f-type-theory
-- Top/TT is unnecessary here actually 

module LobToGoedel

import Data.List.Elem

%default total

data Ty : Type where