Skip to content

Instantly share code, notes, and snippets.

Oleks oleks

Block or report user

Report or block oleks

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
View gist:a0b8c128d12109ca413cedc5da6e3473
$ stack --nix new hello-world -p "category:Compilers/Interpreters"
Downloading template "new-template" to create project "hello-world" in hello-world/ ...
Looking for .cabal or package.yaml files to use to init the project.
Using cabal packages:
- hello-world/
Selecting the best among 14 snapshots...
Unable to load cabal files for snapshot
View gist:e29a4f2fecff2e705bcf2acfd4863df9
// K&R style (according to Rider)
if (condition) {
else {
// One true brace style (1TB)
if (condition) {
View gist:79ced969f38fc193a17037d3bca44f69
OpenJDK 64-Bit Server VM warning: Option UseConcMarkSweepGC was deprecated in version 9.0 and will likely be removed in a future release.
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.intellij.ide.ClassUtilCore to field
WARNING: Please consider reporting this to the maintainers of com.intellij.ide.ClassUtilCore
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
ERROR: null
at java.desktop/java.awt.EventQueue.invokeAndWait(
at java.desktop/java.awt.EventQueue.invokeAndWait(
View gist:03288b7c206d241ef249583d209a2713
$ java --version
OpenJDK Runtime Environment (Zulu build
OpenJDK 64-Bit Server VM (Zulu build, mixed mode)
View Sample.idr
module Sample
import Data.Vect
import Data.SortedMap
X : (n : Nat) -> Type
X n = Vect n Nat
Y : Nat -> Nat -> Type
Y m n = Vect m (X n)
oleks / A.idr
Last active Apr 16, 2017
Defining equality for a non-dependent type hosting a dependent type
View A.idr
module A
import Data.Vect
data T
= Val Int
| Vec (Vect len T)
vectEq : Eq a => Vect n a -> Vect m a -> Bool
vectEq {n} {m} v w = n == m && Just v == (exactLength n w)
oleks / A.idr
Last active Apr 15, 2017
Using dependent types in regular types
View A.idr
module A
import Data.Vect
data T =
MkT (Vect len Int)
eq' : Vect n Int -> Vect m Int -> Bool
eq' {n} {m} v w = n == m && (exactLength n v) == (exactLength n w)
View Spaces.idr
module Spaces
import Lightyear.Char
import Lightyear.Combinators
import Lightyear.Core
import Lightyear.Strings
toomany : Either String (List Char)
toomany = parse (many $ char ' ') " "
View gist:4b12ce8fdbeeeb835fff0670fbf71416
module Expr
data Expr = X
| Plus (Expr, Expr)
Show Expr where
show X = "x"
show (Plus (e_left, e_right)) = (show e_left) ++ " + " ++ (show e_right)
You can’t perform that action at this time.