Skip to content

Instantly share code, notes, and snippets.

View liarokapisv's full-sized avatar

Liarokapis Alexandros liarokapisv

14 followers · 5 following
View GitHub Profile
@liarokapisv
liarokapisv / Test.idr
Last active January 7, 2018 23:24
Show implementation not total
module Test
%default total
data Box : Type -> Type where
MkBox : t -> Box t
data Test : Type where
T1 : Test
T2 : Box Test -> Test
@liarokapisv
liarokapisv / Test.idr
Created January 6, 2018 12:23
Case split
module Test
record Ann where
constructor MkAnn
ann1 : Type
@liarokapisv
liarokapisv / Grammar.idr
Last active January 4, 2018 18:03
Grammar stack overflow
module Test
import Text.Lexer
import Text.Parser
data Token : Type where
AddOp : Token
MulOp : Token
IntConst : Token
@liarokapisv
liarokapisv / SParser.idr
Created January 4, 2018 17:31
State over Grammar
module Danac.Parser
import Danac.Lexer
import Text.Lexer
import Text.Parser
data SParser : Type -> Type -> Bool -> Type -> Type where
MkSParser : (s -> Grammar t c (a, s)) -> SParser s t c a
Functor (SParser s t b) where
@liarokapisv
liarokapisv / dependent.hs
Last active December 11, 2017 15:15
Problem with singletons
import Data.Singletons.Decide
import Data.Singletons.TH
import Data.Kind
@liarokapisv
liarokapisv / ordering.sql
Created September 26, 2017 14:17
Best Practice
select RV.name, MV.title, RT.stars, RT.ratingDate
from (select * from Reviewer) as RV join
(select * from Movie) as MV join
(select * from Rating) as RT on
(RV.rId = RT.rId and RT.mId = MV.mId)
order by RV.name asc, MV.title asc, RT.stars asc