| title | author |
|---|---|
Glassery |
Oleg Grenrus |
After I have
improved the raw performance
of optika – a JavaScript optics library,
it's time to make the library (feature-)complete and sound.
Gathering and classifying all possible optic types, gives us a reference point
| Require Import Vectors.Vector. | |
| Section CT. | |
| Context {F : Type -> Type}. | |
| Record Functor__Dict := { | |
| fmap__ {a b} : (a -> b) -> F a -> F b; | |
| fmap_id__ {t} : forall ft, fmap__ (fun a : t => a) ft = ft; | |
| fmap_fusion__ {a b c} : forall (f : a -> b) (g : b -> c) fa, fmap__ g (fmap__ f fa) = fmap__ (fun e => g (f e)) fa | |
| }. |
| Theorem insert_perm: forall k l, Permutation (k :: l) (insert k l). | |
| Proof. | |
| intros. induction l. | |
| - reflexivity. | |
| - simpl. destruct (ble_nat k a). | |
| + reflexivity. | |
| + transitivity (a :: k :: l). | |
| * apply perm_swap. | |
| * constructor; assumption. | |
| Qed. |
| {-# LANGUAGE RankNTypes, ScopedTypeVariables #-} | |
| import Control.Monad.ST | |
| import Data.Foldable as F | |
| import Data.Array.ST | |
| import Data.Sequence (Seq) | |
| import qualified Data.Sequence as Seq | |
| import Criterion.Main | |