{{ message }}

Instantly share code, notes, and snippets.

# Brendan Zabarauskas brendanzab

Created Sep 7, 2019 — forked from atennapel/CC.hs
Calculus of Constructions, normalization-by-evaluation, semantic typechecking (WIP)
View CC.hs
 data Tm = Var Int | Ann Tm Tm | Abs Tm | App Tm Tm | Pi Tm Tm | Uni deriving (Show, Eq) data Clos = Clos Tm Env deriving (Show, Eq) data Dm = DVar Int | DAbs Clos | DApp Dm Dm | DPi Dm Clos | DUni deriving (Show, Eq) type Env = [Dm] appd :: Clos -> Dm -> Dm appd (Clos b e) t = eval (t : e) b
Last active Jan 27, 2020 — forked from AndyShiue/CuTT.md
Cubical type theory for dummies
View CuTT.md

I think I’ve figured out most parts of the cubical type theory paper(s); I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory? A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then? A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

Q: So what are HIT and UA? A: A HIT is a type equipped with custom equality, as an example, you can write a type similar to the natural numbers but with an equality between all even numbers. Well, it cannot be called natural numbers then.

Last active Sep 27, 2015 — forked from anonymous/playground.rs
Shared via Rust Playground
View swizzle_gen.rs
 fn main() { swizzle_gen(); } fn swizzle_gen() { swizzle_gen0("x"); swizzle_gen0("y"); swizzle_gen0("z"); swizzle_gen0("w"); }
Last active Aug 29, 2015
View glutin-ns-events.rs
 // user application loop { window.poll_events(); } // mac/glutin fn poll_events(&self) { nsapp_waitevent();
Last active Aug 29, 2015 — forked from bvssvni/Main.idr
View error
 rustc src/lib.rs -o idris/idrisfs.o --crate-type=lib --emit=obj Undefined symbols for architecture x86_64: "___morestack", referenced from: _sizeof_int in idrisfs.o sizeof_int::__rust_abi in idrisfs.o mem::size_of::h1f2d9faff57bec09oaa::v0.0 in idrisfs.o ld: symbol(s) not found for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) FAILURE: gcc -O2 -fwrapv -fno-strict-overflow -I. ./idrisfs.o -x c /var/folders/_t/g72k9vzd30b5svvyd1nxpwp40000gn/T/idris5178 -L/Users/sven/Library/Haskell/ghc-7.6.3/lib/idris-0.9.12/share/rts -lidris_rts -lgmp -lpthread -I/Users/sven/Library/Haskell/ghc-7.6.3/lib/idris-0.9.12/share/rts -I. -I/Users/sven/Library/Haskell/ghc-7.6.3/lib/idris-0.9.12/share/prelude -I/Users/sven/Library/Haskell/ghc-7.6.3/lib/idris-0.9.12/share/base -o /var/folders/_t/g72k9vzd30b5svvyd1nxpwp40000gn/T/idris5176
Last active Aug 29, 2015 — forked from bstrie/map.rs
View map.rs
 use std::iter::Iterator; fn map>(fun: |T| -> U, mut iter: I) -> Vec { let mut acc = vec![]; for elt in iter { acc.push(fun(elt)); } acc }
Created Mar 31, 2014 — forked from Aatch/borrow-example.rs
View borrow-example.rs
 extern crate serialize; use serialize::json; fn get_string<'a>(data: &'a json::Json, key: &~str) -> Option<&'a str> { match *data { json::Object(ref map) => { match map.find(key) { Some(&json::String(ref s)) => { Some(s.as_slice())
Last active Dec 22, 2015 — forked from killballad/nest.rs
View nest.rs
 fn new_foo(a: &Path) -> Result<~Foo, ~str> { read_whole_file(a).chain(|b| frob(b)) .chain(|b| baz(b)) .map_move(|b| ~Foo { bar: b }) }
Last active Dec 17, 2015 — forked from andydude/echo.rs
View echo.rs
 use std::{os,str}; fn main() { let args = os::args(); match args.tail() { [~"-n",..strs] => print(str::connect(strs, " ")), strs => println(str::connect(strs, " ")), } }
Last active Dec 15, 2015 — forked from anonymous/RustSyntaxProposal
View rust_syntax_proposal_01.md

The first stage would be to unify the `struct` and `type` keywords.

Current syntax

```struct Name {
first: ~str,
last: ~str
}

struct Point(int, int);```