konn

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, GADTs, DeriveDataTypeable, TypeApplications #-}
data Foo (a :: Maybe b) where { Any :: Foo a; Bang :: Foo (Just t) }
newtype F a (t :: Maybe s) (u :: Foo t)
  = F { runF ::  a} deriving (Show, Eq, Ord, Typeable)
 
 main :: IO ()
 main = print $ typeRep $ Proxy @(F Int ('Just ()) Any)
 -- ~> No instance for (Typeable (F2 Int ('Just ())))

konn

{-# OPTIONS --universe-polymorphism #-}
module Category where
open import Level
open import Relation.Binary
open import Relation.Binary.Core

record IsCategory {c₁ c₂ ℓ : Level} (Obj : Set c₁)
                  (Hom : Obj → Obj → Set c₂)
                  (_≈_ : {A B : Obj} → Rel (Hom A B) ℓ)
                  (_o_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C)

konn

define IsSemigroup(#ty, #mul) =
  (record
    [assoc:
      (-> 
       [a b c: #ty]
       (= #ty 
        ($ #mul a ($ #mul b c))
        ($ #mul ($ #mul a b) c)
       )
      )

konn

{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, KindSignatures #-}
{-# LANGUAGE LiberalTypeSynonyms, RankNTypes, ScopedTypeVariables           #-}
{-# LANGUAGE TypeFamilies, TypeOperators, TypeSynonymInstances              #-}
module ConstraintUnion where
import Data.Kind
import Data.Proxy
import Data.Singletons.Prelude
import Data.Singletons.Prelude.Ord
import Data.Type.Equality
import GHC.TypeNats

konn

use std::marker::PhantomData;

pub trait Nat {
    type Eval;
    fn as_int() -> usize;
}

#[derive(Debug)]
pub struct Zero {}

konn

use std::collections::hash_map::Entry;
use std::collections::HashMap;
use std::hash::Hash;
use std::ops::Fn;

struct Cacher<'a, T, A, B>
where
    T: 'a + Fn(&A) -> B,
    A: 'a,
    B: 'a,

konn

{-# LANGUAGE DeriveAnyClass, DeriveDataTypeable, DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies, FlexibleInstances, MultiWayIf #-}
{-# LANGUAGE TypeFamilies                                      #-}
module Cell where
import Control.Applicative (empty)
import Data.Typeable       (Typeable)
import Data.Word
import Ersatz
import GHC.Generics        (Generic)

konn

{-# LANGUAGE DeriveAnyClass, DeriveDataTypeable, DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies, FlexibleInstances, MultiWayIf #-}
{-# LANGUAGE TypeFamilies                                      #-}
module Cell where
import Control.Applicative (empty)
import Data.Typeable       (Typeable)
import Data.Word
import Ersatz
import GHC.Generics        (Generic)

konn

\ProvidesFile{math-alphabetic.bbx}[2016/02/10 alphabetic biblatex bibliography style for mathematicians]

\RequireBibliographyStyle{alphabetic}
\RequireBibliographyStyle{math-standard}
\ExecuteBibliographyOptions{labelalpha,sorting=anyt}
\endinput

konn

these derivations will be built:
  /nix/store/1kg1v5vy0drxyxq66dvvdwkn1304ifh9-qtwebkit-5.9.1.drv
  /nix/store/ffja7pc88r4wyfk98pi9nk3yha9adblr-qtwebengine-5.10.1.drv
  /nix/store/bzzbb1hrm0dz3rvndyi3mbbxqvyv3mai-python3.6-PyQt-5.10.drv
  /nix/store/k8hyi5ys04x3zhskk7hm9sllxxbj4hmh-python3.6-qtconsole-4.3.1.drv
  /nix/store/nba4gy75da88hd93gvlq4klq3chjya5m-python3.6-jupyter-1.0.0.drv
  /nix/store/asds576kwc2x8zqprh598dvivhnna73b-python3-3.6.5-env.drv
  /nix/store/jspp9rcrxh280wnb3l80f820n9hy94bf-ihaskell-console.drv
  /nix/store/vas9ys522v10834ysxjb2pzxg4lzacdk-ihaskell-nbconvert.drv
  /nix/store/w6hs5ji7dy7j82cw1rh2583ndpn3rgv0-ihaskell-notebook.drv