Skip to content

Instantly share code, notes, and snippets.

Keigo Imai keigoi

Block or report user

Report or block keigoi

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
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.