This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) | |
{- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Spaces | |
import Lightyear.Char | |
import Lightyear.Combinators | |
import Lightyear.Core | |
import Lightyear.Strings | |
toomany : Either String (List Char) | |
toomany = parse (many $ char ' ') " " |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
I hereby claim:
- I am oleks on github.
- I am oleks (https://keybase.io/oleks) on keybase.
- I have a public key whose fingerprint is 851E A9A9 4FB2 6EF2 46D9 5E9A FF3B 19F0 883C DB4E
To claim this, I am signing this object:
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
$ java --version | |
openjdk 9.0.0.15 | |
OpenJDK Runtime Environment (Zulu build 9.0.0.15+181) | |
OpenJDK 64-Bit Server VM (Zulu build 9.0.0.15+181, mixed mode) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 sun.net.www.protocol.jar.JarFileFactory.fileCache | |
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 | |
java.lang.reflect.InvocationTargetException | |
at java.desktop/java.awt.EventQueue.invokeAndWait(EventQueue.java:1328) | |
at java.desktop/java.awt.EventQueue.invokeAndWait(EventQueue.java:1303) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// K&R style (according to Rider) | |
if (condition) { | |
foo(); | |
} | |
else { | |
foo(); | |
} | |
// One true brace style (1TB) | |
if (condition) { |
OlderNewer