llelf

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 [::].

llelf

llelf

   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                 

llelf

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.

llelf

#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));

llelf

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}

module ALaCarte where

llelf

{-# 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

################################################################################
#                                 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

llelf

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:

llelf

{-# 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)