kenji4569

inductive RideStatus
  | requested
  | rejected
  | assigned
  | pickedUp

structure Driver where
  name : String

-- Ride は現在の状態と、必要なら担当ドライバーを持つ。

kenji4569

-- 信号の色を表す型を定義する。
-- `inductive` は、場合の候補を並べて新しい型を作る。
inductive Light
  | red
  | yellow
  | green

-- 次の信号の色を返す関数。
def next
  | Light.red => Light.green

kenji4569

def sum_of_natural_numbers (n : Nat) : Nat :=
  -- 自然数の和を再帰で定義する。
  match n with
  -- 0 までの和。
  | 0 => 0
  -- n + 1 までの和は、n までの和に n + 1 を足す。
  | n + 1 => sum_of_natural_numbers n + (n + 1)

-- 計算例。
#eval sum_of_natural_numbers 5

kenji4569

import re
import subprocess

ASN = "AS200373"

cmd = f"whois -h whois.radb.net -- '-i origin {ASN}'"

result = subprocess.run(
    cmd,
    shell=True,

kenji4569

# # GTFS Viewer

# ## Refs
# - https://gtfs.org/ja/
# - https://www.gtfs.jp/
# - https://nttdocomo-developers.jp/entry/20231218_1

# ## Setup
# $ pip install streamlit streamlit-folium folium pydeck pandas requests geopy gtfs-realtime-bindings
# $ streamlit run gtfs-viewer-app.py

kenji4569

# # Dynamic Vehicle Routing

# ## Refs
# - https://github.com/lb-robotics/python-vehicle-routing
# - https://zenn.dev/ohtaman/articles/streamlit_start_stop

# ## Setup
# $ pip install streamlit numpy scipy pandas altair readerwriterlock
# $ pip install wandb  # Optional. Please do "wandb login" when you use it.
# $ streamlit run dynamic-vehicle-routing-streamlit-app.py

kenji4569

"""
streamlit-folium-example-app

Run the following commands to launch the app:
$ pip install streamlit streamlit-folium
$ streamlit run streamlit-folium-example-app.py

"""

import time

kenji4569

import express from 'express'
import cluster from 'cluster'
import { cpus } from 'os'
import process from 'process'

const workers = Math.min(Number(process.argv[2]) || 1, cpus().length)
const blockTime = Number(process.argv[3])

const app = express()
const port = 4000

kenji4569

kenji4569