{{ message }}

Instantly share code, notes, and snippets.

🍌
semper φ

# Greg Pfeilsellout

🍌
semper φ
Created Apr 11, 2014
View broken-scanl.idr
 scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b scanl f q ls = q :: (case ls of [] => [] x::xs => scanl f (f q x) xs) -- When elaborating left hand side of Main.case block in scanl: -- When elaborating argument ls to Main.case block in scanl: -- Can't unify -- Vect 0 a -- with
Last active Aug 29, 2015
very confused, as usual
View gist:10744574
 import Data.Bits trim : Bits (1 + n) -> Bits n trim b = truncate b BoundedInt : Integer -> Nat -> Type BoundedInt min max = (x : Integer ** so (min <= x && x < toIntegerNat max)) postulate bounds : (x : Integer) -> so (lower <= x && x < toIntegerNat upper) -> so (lower <= x && 1+2*x < pow 2 upper)
Last active Aug 29, 2015
How can I define Ord for integralTy?
View gist:11119737
 integralTy : (signed : Bool) -> Nat -> Type integralTy False 0 = Bits8 integralTy False 1 = Bits16 integralTy False 2 = Bits32 integralTy False 3 = Bits64 integralTy _ _ = Integer inRange : Ord (integralTy m n) => integralTy m n -> integralTy m n -> integralTy m n -> Bool inRange x lower upper = lower <= x && x < upper
Created Apr 24, 2014
View gist:11242089
 (defun ansi-color-insertion-filter (proc string) (when (buffer-live-p (process-buffer proc)) (with-current-buffer (process-buffer proc) (save-excursion ;; Insert the text, advancing the process marker. (goto-char (process-mark proc)) (insert (ansi-color-apply string)) (set-marker (process-mark proc) (point))) (goto-char (process-mark proc)))))
Created Apr 24, 2014
View gist:11242603
 append : Bits m -> Bits n -> Bits (m + n) append {n=n} a b = shiftLeft (cast n) (zeroExtend a) `or` zeroExtend b
Created Apr 24, 2014
View gist:11269679
 (defun ansi-color-insertion-filter (proc string) (when (buffer-live-p (process-buffer proc)) (with-current-buffer (process-buffer proc) (save-excursion ;; Insert the text, advancing the process marker. (goto-char (process-mark proc)) (insert (ansi-color-apply string)) (set-marker (process-mark proc) (point))) (goto-char (process-mark proc)))))
Last active Aug 29, 2015
View gist:11299585
 partition : Bits (m * n) -> Vect m (Bits n) partition {m=Z} _ = Prelude.Vect.Nil partition {m=S m} {n=n} bits = truncate (replace (plusCommutative n (m*n)) bits) :: partition (truncate (shiftRightLogical (cast n) bits))
Created Apr 27, 2014
View gist:11356985
 KeySize : Type KeySize = Fin 256 -- should actually be [1-256], not [0-256] public ARC4Key : KeySize -> Type ARC4Key n = Vect (finToNat n) (Mod 256) -- should be Byte, but can’t convert yet public data AllegedRivestCipher4 : KeySize -> Type where ARC4 : ARC4Key n -> AllegedRivestCipher4 n
Created Apr 28, 2014
My crazy git remotes
View gist:11373682
 \$ git remote -v origin git@github.com:idris-lang/Idris-dev.git (fetch) origin git@github.com:sellout/Idris-dev.git (push) reverse git@github.com:sellout/Idris-dev.git (fetch) reverse git@github.com:idris-lang/Idris-dev.git (push)
Last active Aug 29, 2015
View gist:11390058
 confoundMessage : (StreamCipher k, Serializable i, Serializable o) => k -> i -> o confoundMessage key message = let encodedMsg = encode message in decode (zipWith xor (Prelude.Stream.take (length encodedMsg) (generateKeystream key)) encodedMsg) -- When elaborating an application of function Prelude.Vect.zipWith:
You can’t perform that action at this time.