keigoi

// 記事:
// https://qiita.com/keigoi/items/8ea458e34173dc086e23#%E3%82%BD%E3%83%95%E3%83%88%E3%82%A6%E3%82%A7%E3%82%A2-arduino

// Arduino Studio の設定方法：
// http://trac.switch-science.com/wiki/esp_dev_arduino_ide use esp8266 version 2.2

#include <Servo.h>
#include <ESP8266WiFi.h>

#define SERVO_OFF_PIN 4

keigoi

G ==w==> G          G ==w==> G
-------             -------
π1.G ==w==> π1.G    π2.G ==w==> π2.G
--------------------
G = π1.G  +p  π2.G  ==w==>  G1 +p G2 = G

where subj(w) \cap subj(π1) U subj(π2) = \emptyset

keigoi

moved to https://github.com/keigoi/haskell-cy/blob/main/Cy.hs

keigoi

From mathcomp.ssreflect Require Import all_ssreflect.

Ltac injection_top :=
    match goal with 
    | |- ?x = ?y -> _ => 
      first
        [ by discriminate
        | is_var x; move=>? 
        | is_var y; move=>? 
        | move=>[]

keigoi

type Global = {[L:string]:Local}
type Local = {kind:string; role:string, bra:{[L:string]:Local}}
type Keys<T extends {[L:string]:{}}> = T extends infer U ? keyof U : never;
type Assoc<T extends {[L:string]:{}}, K extends string> = T extends unknown ? K extends keyof T ? T[K] : never : never;
type Force<T extends Local> = 
  [T] extends [Local] 
  ? {kind:T["kind"], role:T["role"], bra:{[X in Keys<T["bra"]>]: Force<Assoc<T["bra"], X>>}} 
  : never

type Comm<R1 extends XS, R2 extends XS, XS extends string, T extends {[L:string]:Global}> = 

keigoi

type GetFoo<T> = [T] extends [{foo:infer R}] ? R : never;
type Foo = GetFoo<{foo:"A"}> // "A"


type GetFoo0<T> = [T] extends [{foo:string}] ? [T] extends [{foo:infer R}] ? R : never : never;
type Bogus = GetFoo0<{foo:"A"}> // unknown ???

  
  
// to remedy this, use indexed type T["foo"]

keigoi

// returns the intersection of all elements in the union T
// i.e. ToIntersect<T1 | T2 | .. | Tn> = T1 & T2 & .. & Tn
type ToIntersect<T> = (T extends unknown ? (x:T) => void : never) extends (x:infer U) => void ? U : never;

// check if T and U are equal
// Here, ([T] extends [U] ? _ : _) suppresses union distribution.
// See: https://github.com/microsoft/TypeScript/issues/29368
type Eq<T,U> = [T] extends [U] ? [U] extends [T] ? true : false : false;

// check if all elements in the union LS are equal by using (T & U) = (T | U) iff T = U

keigoi

import java.util.function.Consumer;
import java.util.function.Function;

public class DualWork {
    // セッション型
    public static class End{
        public End() {}
        public void close() {}
    }
    public static class Send<CONT> {

keigoi

LOAD CSV WITH HEADERS FROM "https://docs.google.com/spreadsheets/u/0/d/1goCfip58Sq7Th_jVwc-wSAvlINxW2XHsxfh16SGHSro/export?format=csv&id=1goCfip58Sq7Th_jVwc-wSAvlINxW2XHsxfh16SGHSro&gid=0" AS line
FIELDTERMINATOR ','
CREATE (p:Patient {
  id:line.id, age:line.age, sex:line.sex, area:line.area,
  confirm_date:line.confirm_date, note:line.note
})
WITH line
MATCH (p:Patient {id:line.id}) MATCH (p0:Patient {id:line.source_id} )
WHERE line.source_id IS NOT NULL
CREATE (p) -[:FROM{link_kind:line.link_kind}]-> (p0);

keigoi

Scribble parallel loop example