This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 (:) [] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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)) | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
data ω : Type₀ where | |
zero : ω | |
suc : ω → ω | |
inf : ω | |
suc-inf : suc inf ≡ inf | |
ω′ : Type₀ | |
ω′ = Maybe ℕ | |
zero′ : ω′ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
init :: [a] -> [a] | |
init xs = foldr f b xs Nothing | |
where | |
b Nothing = error "init: empty list" | |
b _ = [] | |
f x xs Nothing = xs (Just x) | |
f y xs (Just x) = x : xs (Just y) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# OPTIONS --safe --without-K #-} | |
module Bits where | |
infixr 4 _×_ _,_ | |
record _×_ (A : Set) (B : Set) : Set where | |
constructor _,_ | |
field | |
fst : A | |
snd : B |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# OPTIONS --safe --sized-types #-} | |
module Bits where | |
open import Agda.Primitive using (Level) | |
open import Agda.Builtin.Size | |
variable | |
a : Level | |
b : Level |