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.Array | |
import Data.Array.ST | |
import Control.Monad | |
import Control.Monad.ST | |
import Data.Maybe | |
import Data.Functor | |
import Control.Monad.Trans.State | |
f <.> g = liftM f . g |
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
-- This is related to http://stackoverflow.com/questions/27029564/how-do-i-build-a-list-with-a-dependently-typed-length/ | |
{-# LANGUAGE GADTs, KindSignatures, DataKinds, PolyKinds, RankNTypes, TypeOperators #-} | |
import Data.Either | |
import Data.Functor | |
import Control.Monad | |
data Nat = Z | S 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
-- This is related to http://stackoverflow.com/questions/24475546/non-tedious-ast-transformation-proofs-in-agda/ | |
open import Level | |
open import Function | |
open import Relation.Nullary.Core | |
open import Relation.Binary | |
open import Relation.Binary.PropositionalEquality | |
open import Data.Unit | |
open import Data.Bool | |
open import Data.Product hiding (map) |
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 --no-positivity-check #-} | |
open import Level as Le | |
open import Function | |
open import Data.Maybe renaming (map to _<$>_) | |
infixl 4 _<*>_ | |
_<*>_ : ∀ {α β} {A : Set α} {B : Set β} -> Maybe (A -> B) -> Maybe A -> Maybe B | |
just f <*> just x = just (f x) | |
_ <*> _ = nothing |
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 Level as Le | |
open import Function | |
open import Relation.Binary.PropositionalEquality | |
open import Data.Unit | |
open import Data.Product hiding (map) | |
open import Data.Nat as N hiding (_⊔_) | |
open import Data.Vec | |
N-ary-level-Vec' : ∀ {n} -> Vec Level n -> Level -> Level | |
N-ary-level-Vec' = flip $ foldr _ Le._⊔_ |
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
-- This is related to http://stackoverflow.com/questions/26615082/how-does-one-prove-a-type-of-the-form-a-b-in-agda | |
open import Function | |
open import Relation.Binary.PropositionalEquality | |
data Int : Set where | |
Z : Int | |
S : Int -> Int | |
P : Int -> Int |
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
-- totally isomorphic to [], even in a strict monad | |
-- no redundant (<= 0) checks in the `drop' function | |
-- the `zipWith' function is still O(n^2) | |
{-# LANGUAGE Rank2Types #-} | |
{-# LANGUAGE BangPatterns #-} | |
import Data.List | |
import Control.Applicative | |
import Control.Monad |
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 Arith omega.Omega Lists.List. | |
Import ListNotations. | |
Fixpoint ble_nat (n m : nat) : bool := | |
match n with | |
| 0 => true | |
| S n' => | |
match m with | |
| 0 => false | |
| S m' => ble_nat n' m' |
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
(** * Hoare2: Hoare Logic, Part II *) | |
Require Export Hoare. | |
(* ####################################################### *) | |
(** * Decorated Programs *) | |
(** The beauty of Hoare Logic is that it is _compositional_ -- | |
the structure of proofs exactly follows the structure of programs. |
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
-- This is inspired by https://github.com/luqui/experiments/blob/master/Fin-inj.agda | |
open import Function | |
open import Relation.Nullary | |
open import Relation.Binary.PropositionalEquality | |
open import Relation.Binary.HeterogeneousEquality using (refl ; _≅_ ; _≇_ ) | |
open import Data.Empty | |
open import Data.Nat | |
open import Data.Fin as F hiding (_+_) |