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. |
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
Inductive Tree (A : Set) : Set := | |
| Leaf : A -> Tree A | |
| Node : bool -> Tree A * Tree A -> Tree A. | |
Definition subTree {A : Set} (b : bool) (lr : Tree A * Tree A) : Tree A := | |
match (b, lr) with | |
| (true, (a, b)) => a | |
| (false, (a, b)) => b | |
end. |
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 EventT : (event : Type) -> (m : Type -> Type) -> (a : Type) -> Type where | |
MkEventTCont : (event -> m (EventT event m a)) -> EventT event m a | |
MkEventTTerm : m a -> EventT event m a | |
MkEventTEmpty : EventT event m a | |
data LAM : (x : Type) -> Type where | |
App : x -> x -> LAM x | |
Lam : (x -> x) -> LAM x | |
LC : 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
open import Agda.Builtin.Equality | |
open import Agda.Builtin.Nat hiding (_+_; _<_) | |
open import Data.Nat | |
open import Data.Nat.Properties | |
open import Relation.Binary | |
-- C-c C-z RET _*_ _≡_ RET |
NewerOlder