MikuroXina

[hook "clang-format"]
    event = pre-commit
    command = "git clang-format --diff --quiet || (echo 'Run `git clang-format` to fix the errors.'; exit 1)"

MikuroXina

from collections.abc import Callable
from typing import TypeVar

import numpy as np
from numpy.typing import ArrayLike

T = TypeVar("T")
Cont = Callable[[Callable[[ArrayLike], T]], T]
Flow = Callable[[ArrayLike], Cont]
Lens = Callable[[Flow], Flow]

MikuroXina

cmake_minimum_required(VERSION 4.3.1)
cmake_policy(SET CMP0076 NEW)

project(experiment)

add_definitions(-Wall -g)

add_library(list STATIC)
target_compile_features(list PUBLIC cxx_std_20)
target_sources(list PUBLIC

MikuroXina

package cucumbersaregood;

import java.io.File;
import javafx.application.Application;
import javafx.scene.Scene;
import javafx.scene.layout.StackPane;
import javafx.scene.media.Media;
import javafx.scene.media.MediaPlayer;
import javafx.scene.media.MediaView;
import javafx.stage.Stage;

MikuroXina

name: Initialize VRT

on:
  workflow_dispatch:

jobs:
  vrt-init:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

MikuroXina

-- Hilbert-style logic
axiom Ax1 (A B : Prop) : A > (B > A)
axiom Ax2 (A B C : Prop) : (A > (B > C)) > ((A > B) > (A > C))
axiom Ax3 (A B : Prop) : (¬A > ¬B) > (B > A)
axiom Mp (x : A) (f : A > B) : B

theorem Intro {A B : Prop} (y : B) : A > B := by
  have h1 : B > (A > B) := Ax1 B A
  Mp y h1
theorem Mp1 {A B C : Prop} (x : A > B) (y : A > (B > C)) : A > C := by

MikuroXina

/-
  NAND 演算子 `↑` からなる計算系. `A` は「A が真」を, `A ↑ A` は「A が偽」を意味する.
  `A ↑ B` は「A と B が同時に真にならない」あるいは「A と B のいずれかが偽」を意味する.
-/
def nand (a b : Prop): Prop := ¬(a ∧ b)
infix:65 " ↑ " => nand

variable {A B C : Prop}

/--

MikuroXina

package main

type OptionHandlers[T any, R any] struct {
	OnSome func(value T) R
	OnNone func() R
}
type Option[T any] func(handlers OptionHandlers[T, any]) any

func Some[T any](value T) Option[T] {
	return func(handlers OptionHandlers[T, any]) any {

MikuroXina

責任を負うものについて、話したことがありましたね。
先生は、シッテムの箱のシステム管理者であるA.R.O.N.Aさんから
次の3点について講習を受けませんでしたか？
    #1) 他人のプライバシーを尊重すること。
    #2) タイプする前に考えること。
    #3) 大きな力には大いなる責任が伴うこと。

？「にははは……！大きな力だあ……！え？大いなる責任？なんですかそれ？」

MikuroXina

#[derive(Debug, Clone)]
enum Expr {
    Int(u32),
    Succ,
    Apply(Box<Expr>, Box<Expr>),
    Comp(Box<Expr>, Box<Expr>),
    Times(Box<Expr>, Box<Expr>),
}

enum ExprRes {