Skip to content

Instantly share code, notes, and snippets.


Sven Nilsen bvssvni

View GitHub Profile
bvssvni / bottles_of_beer.dyon
Created Dec 20, 2018
99 bottles of beer (in Dyon)
View bottles_of_beer.dyon
fn main() {
n := 99
println(link {
link i n {
b := n-i
bottles(b)" of beer on the wall, "bottles(b)" of beer.\n"
"Take one down, pass it around, "bottles(b-1)" of beer on the wall.\n\n"
"No more bottles of beer on the wall, no more bottles of beer.\n"
"Go to the store and buy some more, "n" bottles of beer on the wall.\n"
bvssvni / philosophers.txt
Created Feb 24, 2018
Philosophers and thinkers communication style described with a single sentence
View philosophers.txt
Albert Einstein - His genius papers are never read by common people, but they absorb every sentence he ever said publicly.
Bertrand Russel - He was the center of the logical revolution of mathematics, but his gentleman appearance hides his colorful life.
Daniel Dennett - Smart, knows a lot and good at talking about interesting things. He is the center.
Eliezer Yudkowsky - The world collides with him, he loves it, he attacks it straight on, and the world loses ... every time.
Elon Musk - A cool idea that sounds like one came up with it while playing on the boy's room, but real.
bvssvni /
Last active Oct 13, 2017
Unhyping AI Jokes

Bayesian reasoning, no temporal logic

Operator: Computer, the door is open, the door is closed. Is the door closed?
Computer: I don't know!

Monotonic solver, no temporal logic, no assumption checking

Operator: Computer, the door is open, the door is closed. Is the door open?
Computer: Yes!
Operator: Computer, is the door closed?


Bayesian reasoning, no temporal logic

Operator: Computer, the door is open, the door is closed. Is the door closed? Computer: I don't know!

Temporal logic, no Bayesian reasoning

Operator: Computer, the sky is green, the sky is blue. Which color has the sky? Computer: It was green, but changed to blue right now.

bvssvni / add_even.idr
Created Apr 6, 2017
Managed to prove the path `add[even] <=> eq`
View add_even.idr
prove_add_even : (x : Nat) -> (y : Nat) -> even (add x y) = eq (even x) (even y)
prove_add_even Z Z = Refl
prove_add_even Z (S Z) = Refl
prove_add_even Z (S (S k)) = prove_add_even Z k
prove_add_even (S Z) Z = Refl
prove_add_even (S (S k)) Z = prove_add_even k Z
prove_add_even (S Z) (S Z) = Refl
prove_add_even (S Z) (S (S k)) = prove_add_even (S Z) k
prove_add_even (S (S k)) (S j) = prove_add_even k (S j)
bvssvni / test.idr
Created Apr 4, 2017
Attempt to generate a function type
View test.idr
data PathType = NAT | BOOL
interpPathType : PathType -> Type
interpPathType NAT = Nat
interpPathType BOOL = Bool
Func : Type
Func = (List PathType, PathType)
interp : Func -> Type
bvssvni /
Last active Jan 17, 2017
YEAH! It compiles!
pub fn par_trans2(
pos: V2<f32>,
f: Box<Fn(&[V2<f32>], &mut [bool]) + Sync>
) -> Box<Fn(&[V2<f32>], &mut [bool]) + Sync>{
const SIZE: usize = 1024;
Box::new(move |input, output| {
.for_each(|(i, o): (&[V2<f32>], &mut [bool])| {
/// Use stack memory to avoid allocations.
bvssvni /
Created Jan 15, 2017
LLVM takes a long time to optimize this
extern crate piston_meta;
extern crate range;
extern crate dyon;
use std::sync::Arc;
use self::piston_meta::MetaData;
use self::range::Range;
use self::dyon::{error, load_meta, Module, Runtime};
fn main() {
View gist:10a1cf737fcea6feca2a14c79bf05767
$ cargo publish --verbose
Updating registry ``
error: failed to update registry
Caused by:
failed to fetch ``
Caused by:
[9/-3] Object not found - no match for id (af86e67bfa42abc6f7362a4f1de845b4e3a943f3)
bvssvni / syntax.txt
Created Jan 3, 2017
Syntax for a subset of English that is activity focused
View syntax.txt
_seps: "."
8 sentence = [activity:"activity" .w? "."]
9 expression = .s!([.w! {"&":"&" "|":"|"} .w!] activity:"term")
10 if = [{"if" "when"} .w! expression:"condition" .w! "then" .w! expression:"then"
.r?([.w! "else" .w! "if" .w! expression:"else_if_condition" .w!
"then" .w! expression:"else_if_then"])
?[.w! "else" .w! expression:"else"]]
11 activity = [!{"then" "else" "&" "|"} {