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 TypeFamilies #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
module Deriving where | |
import Data.Kind (Type) | |
newtype Cst a i = MkCst { runCst :: a } | |
newtype Idt i = MkIdt { runIdt :: i } | |
newtype Prd k l i = MkPrd { runPrd :: (k i, l i) } |
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 #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE TypeAbstractions #-} | |
{-# LANGUAGE TypeApplications #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
import Control.Concurrent (forkIO, MVar, newEmptyMVar, putMVar, takeMVar) | |
import Data.Kind (Type) |
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
module ShaSearch where | |
import System.Process (readProcess) | |
----------------------------------------------- | |
-- Using the list monad to generate all the | |
-- hexadecimal words of a given length | |
-- All the hexadecimal characters | |
hexa :: [Char] |
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
module Rot13 where | |
import Control.Monad (guard) | |
import Data.Char (ord, chr, toLower, isLower) | |
import Data.Function (on) | |
import Data.List (sortBy) | |
import Data.Maybe (mapMaybe) | |
import Data.Set (Set) | |
import qualified Data.Set as Set |
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
module Error | |
export | |
data Error : (err, a : Type) -> Type where | |
MkError : (forall r. (err -> r) -> (a -> r) -> r) -> Error err a | |
export %inline | |
runError : Error err a -> (err -> r) -> (a -> r) -> r | |
runError (MkError hdl) kE kV = hdl kE kV |
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
module LambdaLetRec | |
import Data.List1 | |
import Data.List.Quantifiers | |
-------------------------------------------------------------------------------- | |
-- types | |
infixr 5 ~> |
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 Data.String | |
import Data.List | |
import Data.List.Elem | |
import Decidable.Decidable | |
import Decidable.Equality | |
%default total | |
toWitness : (prf1 : Dec a) -> IsYes prf1 -> a | |
toWitness (Yes prf2) x = prf2 |
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
open import Agda.Builtin.Size | |
open import Data.Maybe.Base | |
data List {n} (T : Set n) (i : Size) : Set n where | |
[] : List T i | |
_∷_ : ∀ {j : Size< i} → T → List T j → List T i | |
data Smaller {n} (T : Size → Set n) (i : Size) : Set n where | |
[_] : {j : Size< i} → T j → Smaller T i |
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 SyntaxDesc (I : Set) where | |
open import Agda.Primitive using () renaming (Set to Type) | |
open import Data.Nat.Base | |
open import Data.Fin.Base | |
open import Data.List.Base using (List; []; _∷_; _++_) | |
data Desc : Type₀ 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
Require Import List. | |
Inductive PalAcc {A : Type} (acc : list A) : list A -> Type | |
:= Even : PalAcc acc acc | |
| Odd : forall x, PalAcc acc (x :: acc) | |
| Step : forall x xs, PalAcc (x :: acc) xs -> PalAcc acc (x :: xs) | |
. | |
Definition Pal {A : Type} (xs : list A) : Type := PalAcc nil xs. |
NewerOlder