oisdk

{-# OPTIONS --without-K #-}

module ReductionProblem where

open import Agda.Builtin.Nat using (Nat; suc; zero)
open import Agda.Primitive using (_⊔_)
open import Agda.Builtin.Equality using (_≡_; refl)

-- The Acc type, defined as a record:
record Acc {a r} {A : Set a} (R : A → A → Set r) (x : A) : Set (a ⊔ r) where

oisdk

{-# LANGUAGE UnicodeSyntax        #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import Data.Functor.Const

oisdk

-- Selective lets us do "monadic" binds where the domain is restricted
-- to the countable types (which can be infinite).

{-# LANGUAGE TypeOperators     #-}
{-# LANGUAGE PatternSynonyms   #-}
{-# LANGUAGE ViewPatterns      #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts  #-}

import GHC.Generics

oisdk

{-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds, RankNTypes, ScopedTypeVariables, TypeOperators  #-}

import Data.Kind
import Data.Coerce

data Nat = Z | S Nat

data Vec (a :: Type) (n :: Nat) where
  Nil :: Vec a Z
  (:-) :: a -> Vec a n -> Vec a (S n)

oisdk

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveFoldable, DeriveTraversable, DeriveFunctor #-}

import Data.List (mapAccumL)

data Stream a = a :< Stream a deriving (Functor, Foldable, Traversable)
infixr 5 :<

instance Show a => Show (Stream a) where
  showsPrec n = showsPrec n . foldr (:) []

oisdk

import Test.QuickCheck
import Data.Tree.Binary.Preorder (Tree(..), drawTree)
import Control.Arrow (first)
import Data.List (unfoldr)

fromList :: [a] -> Tree a
fromList xs = head (l (foldr f b xs 1 2))
  where
    b _ _ ys zs = (repeat Leaf, (repeat Leaf, ys))
    

oisdk

{-# LANGUAGE DeriveFunctor, LambdaCase, BlockArguments, BangPatterns, RankNTypes, GeneralisedNewtypeDeriving, OverloadedLists, TypeFamilies #-}

{-# OPTIONS_GHC -Wall #-}

import Control.Monad
import Control.Applicative
import Numeric.Natural
import GHC.Exts
import GHC.Base (build)

oisdk

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, NoStarIsType #-}

{-# OPTIONS_GHC -Wall -fno-warn-unticked-promoted-constructors #-}

import Data.Monoid (Sum(..))
import Data.Kind (Type)

data Nat = Z | S Nat

data Fin (n :: Nat) where

oisdk

{-# OPTIONS --cubical --safe #-}

module Curry where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function

open import Cubical.Data.Nat

oisdk

data ω : Type₀ where
  zero : ω
  suc : ω → ω
  inf : ω
  suc-inf : suc inf ≡ inf

ω′ : Type₀
ω′ = Maybe ℕ

zero′ : ω′