{{ message }}

Instantly share code, notes, and snippets.

🤦

# Antonio Nikishaevllelf

🤦
Last active May 16, 2020
View program+qc.v
 From QuickChick Require Import QuickChick. From Coq Require Import Program. From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool eqtype seq. Program Fixpoint itakep {A} (n:nat) (s:seq A) {measure n} : seq A := if s isn't [::] then (if n <= size s as r return (n <= size s = r -> _) then fun pf => take n s else fun pf => s ++ itakep (n - size s) s) erefl else [::].
Last active Apr 30, 2020
Last active Oct 12, 2020
View folds
 what k4/k7 k9 example result --------------------------------------------------------------------------------- each-left a f\:b a f\:b (!3)*\:!2 (0 0;0 1;0 2) each-right a f/:b a f/:b (!3)*/:!2 (0 0 0;0 1 2) fold f/v f/v */6 7 42 fold w/initial a f/v a f/v 7*/11 13 1001 scan f\v f\v -\1 1 1 1 0 -1 scan w/initial a f\v a f\v 3-\1 1 1 2 1 0
Created Apr 28, 2020
View koq.v
 Module I32:=Int. Module I64:=Int64. Notation i32:=I32.int. Notation i64:=I64.int. Notation "[i32 i ]" := (I32.mkint i _)(format "[i32 i ]"). Notation "[i64 i ]" := (I64.mkint i _)(format "[i64 i ]"). Section core. Inductive Nu := I of i32 | J of i64. Inductive At := ANu of Nu | AC of ascii. Inductive Ty := Ti|Tj|TL|Tc.
Last active Apr 27, 2020
View ktn.c
 #define KXVER 3 #include"k.h" #include #define PK(s,x) O("%15s: %p[r=%d] n=%lld %d..\n",s,x,x->r,x->n,*kI(x)) I main(){ I i=42; K top1=ktn(KI,0), top2=ktn(KI,0), v=ktn(KI,0); jk(&top1,r1(v)); jk(&top2,r1(v));
Last active Sep 5, 2019 — forked from dredozubov/alacarte.hs
View alacarte.hs
 {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeApplications #-} module ALaCarte where
Created May 3, 2018 — forked from sjoerdvisscher/liftedMonoid.hs
If you have a Functor f with an instance Monoid a => Monoid (f a), f is Applicative!
View liftedMonoid.hs
 {-# LANGUAGE TypeOperators, ScopedTypeVariables, TupleSections #-} import Data.Constraint import Data.Monoid import Control.Applicative pureDefault :: forall f a. Functor f => (Monoid () :- Monoid (f ())) -> a -> f a
Created Sep 15, 2017
Block OSX El Capitan from phoning home
View etc-hosts
 ################################################################################ # PRIVACY RULES # # * OSX EL CAPITAN - NO CONNECTIONS TO CUPPERTINO * # # MIX OF DIFFERENT /etc/hosts FILES I'VE FOUND. 80% OF THE ENTRIES CAME FROM # # MY OWN. OSX SENDS HUGE AMMOUNT OF REQUESTS TO CUPPERTINO EVENT WHEN # # SPOTLIGHT SUGGESTIONS, ICLOUD, AND OTHER SERVICES ARE DISABLED # # USE IT IF YOU DON'T LIKE OSX CALLING HOME WHEN YOU DON'T WANT IT TO HAPPEN # # NO CONNECTIONS TO APPLE SERVERS REPORTED BY MY FIREWALL FOR 2 MONTHS # ################################################################################ # SAVED FROM: http://pastebin.com/GfaXGL4r
Created Jan 12, 2017
View keybase.md

### Keybase proof

I hereby claim:

• I am llelf on github.
• I am lelf (https://keybase.io/lelf) on keybase.
• I have a public key ASCut-M2ylTC8ta3u74-HP2XbSgF7j7D3u4TTPIObH4YOwo

To claim this, I am signing this object:

Last active Mar 14, 2020
View ip1.hs
 {-# LANGUAGE GADTs, ConstraintKinds, Rank2Types, ImplicitParams #-} data Rec fields where Rec :: fields => Rec fields infixr 1 ? (?) :: Rec fields -> (fields => r) -> r Rec ? e = e record :: Rec (?a :: Int, ?b :: String)
You can’t perform that action at this time.