Skip to content

Instantly share code, notes, and snippets.

Avatar
🤦

Antonio Nikishaev llelf

🤦
View GitHub Profile
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 [::].
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
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.
View ktn.c
#define KXVER 3
#include"k.h"
#include<stdio.h>
#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));
View alacarte.hs
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
module ALaCarte where
@llelf
llelf / liftedMonoid.hs
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
@llelf
llelf / etc-hosts
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
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:

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.