Skip to content

Instantly share code, notes, and snippets.

Nicolas B. berewt

Block or report user

Report or block berewt

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@berewt
berewt / Audit.idr
Created Jun 17, 2018
Data pre-processing in Idris with the version 0.0.1 of Leon
View Audit.idr
module Audit
import Control.Monad.Syntax
import Data.Fin
import Data.String
import Data.Vect
import Data.Vect.Sub
import Leon.DataFrame.Columns
@berewt
berewt / TennisDT.idr
Last active May 26, 2018
Tennis Kata, in Idris, with Dependent types.
View TennisDT.idr
module TennisDT
%default total
data Player = Player1 | Player2
||| Prove that the game is not over after a point
data NotWinning : Nat -> Nat -> Type where
||| Game is not over because the winning player is below 40
View ITE.hs
module Pipes.ITE where
import Pipes
import qualified Pipes.Prelude as P
ite :: Monad m => (a -> Bool) -> Pipe a b m () -> Pipe a c m () -> Pipe (Either b c) d m () -> Pipe a d m r
ite predicate l r j = for cat $ \x -> yield x >-> if predicate x
then l >-> P.map Left >-> j
else r >-> P.map Right >-> j
View ArduinoBasic.idr
||| A Straightforward translation of the
||| [ArduinoML](https://github.com/mosser/ArduinoML-kernel) use case
||| with a bit of syntax extension for a smooth DSL experience
module ArduinoBasic
import Data.Union
namespace model
data SIGNAL = LOW | HIGH
View VerifiedSmartConstructor.idr
module Main
||| The smart consturctor tool:
||| Check whether an element belongs to a given subset
subset : ((x: a) -> Dec (prop x)) -> a -> Either a (Subset a prop)
subset dec y with (dec y)
| (Yes prf) = pure (Element y prf)
| (No contra) = Left y
-- Example
View NodeLeafTree.hs
module NodeLeafTree where
import Data.Bifunctor
import Data.List.NonEmpty
data Tree a b
= Leaf a
| Node b (NonEmpty (Tree a b))
instance Bifunctor Tree where
View ObjectLiteralDumbass.js
$ node --version
v6.9.1
$ node
> bar = {MyClass: function (x) {this.x = x}}
{ MyClass: [Function: MyClass] }
> foo = {MyClass(x) {this.x = x}}
{ MyClass: [Function: MyClass] }
> new bar.MyClass(2)
MyClass { x: 2 }
> new foo.MyClass(2)
@berewt
berewt / Union.idr
Created Jul 22, 2016
Union type in Idris
View Union.idr
module Data.Union
import Data.Vect
data Sum : {n: Nat} -> Vect n Type -> Type where
isA: t -> {auto e: Elem t ts} -> Sum ts
data Orange = AnOrange String
data Apple = AnApple String
@berewt
berewt / TDT.hs
Last active Sep 3, 2015
Duck Typed morphisms statically typed
View TDT.hs
{import Control.Applicative ((<|>))
import Control.Monad
import Data.Data
import Data.Generics.Aliases
import Data.Monoid
trans :: (MonadPlus m, Typeable a, Typeable b) => (b -> r) -> a -> m r
trans = mkQ mzero . (return .)
mcast :: (Typeable b, Typeable r) => (a -> Maybe b) -> a -> Maybe r
You can’t perform that action at this time.