lukenels

Keybase proof

I hereby claim:

• I am lukenels on github.
• I am lukenels (https://keybase.io/lukenels) on keybase.
• I have a public key ASCH3oJ-h1xhVH89PjDxidgqY39gNYInpUdBtkk1_l0YAAo

To claim this, I am signing this object:

lukenels

#
# Automatically generated file; DO NOT EDIT.
# Linux/x86 4.13.0-rc1 Kernel Configuration
#
CONFIG_64BIT=y
CONFIG_X86_64=y
CONFIG_X86=y
CONFIG_INSTRUCTION_DECODER=y
CONFIG_OUTPUT_FORMAT="elf64-x86-64"
CONFIG_ARCH_DEFCONFIG="arch/x86/configs/x86_64_defconfig"

lukenels

{-# LANGUAGE RankNTypes,
             GADTs,
             TypeInType,
             TypeFamilies,
             EmptyCase #-}


{- Logic -}

lukenels

data M b = M (M b -> b)

runM :: M b -> M b -> b
runM (M x) = x

omega :: a
omega = (\x -> runM x x) $ M (\x -> runM x x)

lukenels

import z3

hearts_8 = z3.Int('8 of Hearts')
diamonds_10 = z3.Int('10 of Diamonds')
club_king = z3.Int('King of Clubs')
spades_10 = z3.Int('10 of Spades')
diamonds_queen = z3.Int('Queen of Diamonds')

cards = [hearts_8, diamonds_10, club_king, spades_10, diamonds_queen]

lukenels

Require Import String.
Require Import List.

Inductive hlist : list Set -> Type :=
| hnil : hlist nil
| hcons : forall (x: Set) (xs: list Set), x -> hlist xs -> hlist (x :: xs).

Fixpoint hlist_builder (n: nat) (l: list Set) :=
  match n with

lukenels

newtype M b = M { runM :: (M b) -> b }

u = \f -> f (\x y -> x) (\x y z -> x z (y z)) (\x y -> x)

fix :: (a -> a) -> a
fix = ((u (u u)) ((u u u) (u (u u))) (u u u)) (((u (u u)) (u (u u)) ((u (u u)) (u u u)))
      (((u (u u)) ((u (u u)) ((u u u) ((u (u u)) ((u u u) (u (u u))) (u u u))) (u (u u)))
      ((u u u) (u u u))) ((u (u u)) ((u u u) (u (u u))) (u u u)) M)) (((u (u u)) ((u u u)
      (u (u u))) (u u u)) (((u (u u)) ((u u u) (u (u u))) (u u u)) ((u (u u)) (u (u u))

lukenels

newtype M b = M { runM :: (M b) -> b }

fix :: (a -> a) -> a
fix = ((const (<*>)) <*> const) (((<*>) <*> ((<*>) const))
      ((const ((const (<*>)) <*> const) <*> (<*>) <*> (const const))
      ((const (<*>)) <*> const) M))
      (((const (<*>)) <*> const) (((const (<*>)) <*> const) ((<*>) <*> ((<*>) const))
      ((const ((const (<*>)) <*> const) <*> (<*>) <*> (const const))
      ((const (<*>)) <*> const) runM)) ((const (<*>)) <*> const))

lukenels

Require Import String.
Require Import List.
Require Import Permutation.

  Inductive expr : Set :=
  | atom : string -> expr
  | dual_atom : string -> expr

  | mul_conj : expr -> expr -> expr