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
convert: item __std_macros with id 4 rp None | |
convert: item SearchEngine with id 6 rp None | |
write_ty_to_tcx(6, SearchEngine) | |
write_ty_to_tcx(7, std::hashmap::HashMap<~str,~str>) | |
convert: item __extensions__ with id 16 rp None | |
write_ty_to_tcx(16, SearchEngine) | |
ty_of_bare_fn | |
write_ty_to_tcx(65, extern "Rust" fn() -> ~std::iter::Iterator<std::send_str::SendStr><no-bounds>) | |
convert: item main with id 67 rp None | |
ty_of_bare_fn |
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
#include <vector> | |
#include <iostream> | |
template<typename T, int i> | |
struct Conditional { | |
typedef T Type; | |
}; | |
template<typename T> | |
struct Conditional<T, 0>; |
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 type Type = sig | |
module type T | |
end | |
module Equality = (struct | |
module Eq(Typ:Type)(X:Typ.T)(Y:Typ.T) = struct | |
module type T = sig end | |
end | |
module Eq_refl(Typ:Type)(X:Typ.T) = (struct |
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
(* Dimensional analysis in OCaml, using only Hindley-Milner | |
with variance annotations! | |
The technique for representing typelevel integers that we use | |
here is from the talk "Many Holes in Hindley-Milner", by | |
Sam Lindley (http://www.kb.ecei.tohoku.ac.jp/ml2008/slides/lindley.pdf) *) | |
(* This type needs to be covariant so we can | |
generalize one : ('_a, '_a suc) int to ('a, 'a suc) int *) | |
(* It is also necessary to make it concrete so we don't | |
allow circular types such as ( 'a suc as 'a, 'a ) int *) |
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
validParentheses = (== 1) . foldl (flip ($)) 1 . map (\case { '(' -> (* 2); ')' -> (`div` 2) }) |
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
import std.stdio; | |
import std.algorithm; | |
mixin template VarDecl(T, alias string VarName) { | |
mixin (`private T `~VarName~`;`); | |
mixin (`T get_`~VarName~`() { return this.`~VarName~`; }`); | |
mixin (`void set_`~VarName~`(T value) { this.`~VarName~` = value; }`); | |
} | |
class Klass { |
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
package starfighter.types | |
sealed abstract class TList | |
sealed class TNil extends TList | |
sealed class TCons[A, B <: TList] extends TList | |
object TList { | |
type L[A] = TCons[A, TNil] | |
type ::[A, B <: TList] = TCons[A, B] | |
} |
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
exception Found_element of int | |
let find_first (p : int -> bool) (s : int Stream.t) = | |
try ( | |
Stream.iter (fun elt -> if p elt then raise (Found_element elt)) s; | |
None | |
) | |
with | |
Found_element elt -> Some elt |
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
-- type-in-type is unlikely to be necessary, but it does make my life easier. | |
{-# OPTIONS --type-in-type #-} | |
module Scott where | |
open import Function | |
open import Relation.Binary.PropositionalEquality | |
open ≡-Reasoning | |
open import Data.Product | |
open import Data.Sum |
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 type Iter = sig | |
type 'a coll | |
type 'a t | |
val iter : 'a coll -> 'a t | |
val next : 'a t -> ('a * 'a t) option | |
end | |
module IterLemmas(I : Iter) = struct | |
let fold (x: 'a) (f: 'a -> 'b -> 'a) (coll: 'b I.coll) = |