LeifW

{-# LANGUAGE OverloadedStrings #-}
module Main where

import Data.Avro
import Data.Avro.Schema

data Thing = Thing { num :: Int }

thingSchema :: Schema
thingSchema = Record "Thing" Nothing [] Nothing Nothing

LeifW

mappings in (Compile, packageBin) ++= Def.taskDyn {
  val schemaFolder = (target in Compile).value / "generatedSchemas"
  Def.task {
    (run in Compile).toTask(" " + schemaFolder).value
    schemaFolder.listFiles.toSeq map (f => f -> f.getName)
  }
}.value

LeifW

natAssoc1 : (x, y, z : Nat) -> x + (y + z) = (x + y) + z
natAssoc1 = ?natAssocProof

natAssocProof = proof
  intros
  induction x
  trivial
  intros
  compute
  rewrite ihn__0

LeifW

	Optional	Either	CompletableFuture
Create success value	Optional.of	Either.right	CompletableFuture.completedFuture
Create failure value	Optional.empty	Either.left	f = new CompletableFuture(); f.completeExceptionally; return f
Apply function to success case	.map	.map	.thenApply
Apply a function to success case that may also fail	.flatMap	.flatMap	.thenCompose
Handle both failure & sucess cases at once	.map().orElse()	.fold	.handle

LeifW

{-# LANGUAGE OverloadedStrings #-}
import Network.Wai
import Network.HTTP.Types
import Network.Wai.Handler.Warp (run)
--
import Control.Concurrent (threadDelay)
import Data.Atomics.Counter --(newCounter, incrCounter)

app :: AtomicCounter -> Application
app counter _ respond = do

LeifW

AST.hs:92:15: error:
    • No instance for (Data.Functor.Classes.Eq1 Expr)
        arising from the third field of ‘Module’ (type ‘Decls a’)
      Possible fix:
        use a standalone 'deriving instance' declaration,
          so you can specify the instance context yourself
    • When deriving the instance for (Eq (Module a))

AST.hs:92:35: error:
    • No instance for (Data.Functor.Classes.Ord1 Expr)

LeifW

{-# Language OverloadedStrings #-}

import Git
import Git.Libgit2 (lgFactory)
import Data.Tagged

gitStuff = do
  Just ref <- resolveReference "HEAD"
  commit <- lookupCommit $ Tagged ref
  history <- lookupCommitParents commit

LeifW

plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)

-- Base case
(O + m = m + O) <== plus_comm = 
    rewrite ((m + O = m) <== plusZeroRightNeutral) ==> 
            (O + m = m) in refl

-- Step case
(S k + m = m + S k) <== plus_comm =
    rewrite ((k + m = m + k) <== plus_comm) in

LeifW

%default total

data MyEq : a -> a -> Type where
  MyRefl : MyEq a a

myTrans : MyEq a b -> MyEq b c -> MyEq a c
myTrans MyRefl MyRefl = MyRefl

LeifW

FROM nfnty/arch-mini

RUN pacman -Sy --noconfirm --needed git cabal-install ghc libffi pkg-config make sed grep
RUN cabal update
RUN git clone https://github.com/idris-lang/Idris-dev.git
RUN cd Idris-dev && cabal -fFFI -fGMP install