Skip to content

Instantly share code, notes, and snippets.

Avatar

Keigo Imai keigoi

View GitHub Profile
View covid_link_db.cypher
@keigoi
keigoi / README.md
Last active Nov 22, 2019
Scribble parallel loop example
View README.md

Scribble parallel loop example

@keigoi
keigoi / lens.ts
Last active Nov 9, 2018
lens typescript
View lens.ts
function id<A>(x:A): A {
return x;
}
abstract class Lens<V1, V2, S1, S2> {
abstract get(s: S1): V1;
abstract put(s: S1, v:V2) : S2
}
@keigoi
keigoi / adder_protocol.ml
Created Oct 21, 2018
Channel vector generation from Scribble protocol
View adder_protocol.ml
(*
module fase16.adder.Adder;
type <ocaml> "int" from "stdlib" as Int;
global protocol Adder(role C, role S)
{
choice at C
{
Add(Int, Int) from C to S;
Res(Int) from S to C;
do Adder(C, S);
View mpst.ml
module type S = sig
type _ mpst
type _ sess
type (_, _, _, _) lens
type (_, _) label
type (_, _, _, _) dlabel
type ('a, 'b, 'c, 'd, 'e, 'f) role = ('a, 'b, 'c, 'd) lens * ('e, 'f) label
type _ typ
View Android_Studio_project_on_network_drive.md
View metasession.ml
module M : sig
type 'a t
val return : 'a code -> 'a t
val (>>=) : 'a t -> ('a code -> 'b t) -> 'b t
val go : unit t -> unit code
end = struct
type 'a t = ('a -> unit) code -> unit code
let return = fun a k -> .< .~k .~a >.
let (>>=) m f = fun k -> .< .~(m .< fun x -> .~(f .< x >. k) >. ) >.
let go : unit t -> unit code = fun m -> m .< fun () -> () >.
View metaocamltest.ml
module M : sig
type 'a t
val return : 'a code -> 'a t
val (>>=) : 'a t -> ('a code -> 'b t) -> 'b t
val go : unit t -> unit code
end = struct
type 'a t = ('a -> unit) code -> unit code
let return = fun a k -> .< .~k .~a >.
let (>>=) m f = fun k -> .< .~(m .< fun x -> .~(f .< x >. k) >. ) >.
let go : unit t -> unit code = fun m -> m .< fun () -> () >.
View sum.v
Require Import Nat.
Require Import Omega. (* fixme *)
Fixpoint sum (n:nat) : nat :=
match n with
| O => O
| S n => S n + sum n
end.
Lemma sum_double : forall (n:nat), sum n * 2 = n * (n + 1).
View dependent_rewrite.v
(* check the behaviour of Coq's rewrite tactics *)
Parameter T : Type.
Lemma mmm1 : forall (x y:T) (p : x = y),
existT (fun (y':T) => x = y') y p = existT (fun (y':T) => x = y') x (eq_refl x).
Proof.
intros.
rewrite p.
reflexivity.
You can’t perform that action at this time.