MikuroXina’s gists

MikuroXina / hilbert.lean

Created November 15, 2025 11:17

Hilbert-style calculus proofs for [The Incredible Proof Machine](https://incredible.pm/).

	-- 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.lean

Created November 14, 2025 10:35

NAND calculus proofs for [The Incredible Proof Machine](https://incredible.pm/).

	/-
	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 / option.go

Created October 26, 2025 16:20

An incomplete experiment of Option (Maybe) monad in Go language.

	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 / gsc_president.lecture

Created October 16, 2025 11:40

A lecture file inspired by Blue Archive.

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

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

MikuroXina / dunno.rs

Created August 1, 2025 19:40

An interpreter of Dunno.

	#[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 {

MikuroXina / bench.rs

Created July 11, 2025 04:07

Simple back copy vs memmove in Rust.

	//! Execution result:
	//! ```
	//! running 2 tests
	//! test bench1 ... bench: 0.31 ns/iter (+/- 0.00)
	//! test bench2 ... bench: 0.34 ns/iter (+/- 0.09)
	//! ```

	#![feature(test)]

	extern crate test;

MikuroXina / subtitle_placer.lua

Last active June 26, 2025 10:52

Subtitle Text+ clips auto-placer for DaVinci Resolve. It needs to place audio clips manually, but automates corresponding subtitles from your template caption Text+ clip.

	-- Original: https://zenn.dev/kirimin/articles/3abcada2b1646f by kirimin https://github.com/kirimin

	-- convention of voice/text file: "num_character_content" + ".wav" or ".txt"

	-- Replace configs here
	local TEXT_DIR = "/Users/mikuroxina/Documents/Projects/Scripts/pencil-puzzles/05/voices/" -- folder contains txt and wav
	local AUDIO_TRACK = 2 -- number of audio track placed character voices
	local CHARACTERS = { "中国うさぎ" } -- names of character, used in file name

	-- --------------------------------------------------

MikuroXina / int.rs

Last active June 24, 2025 01:54

Type level integer with phantom types in Rust.

	use std::marker::PhantomData;

	#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
	pub enum Z {}
	#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
	pub struct S<Z>(PhantomData<Z>);

	/// `Int<M, N>` represents an integer `M - N`.
	#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
	pub struct Int<M, N>(i64, PhantomData<(M, N)>);

MikuroXina / ceil_sqrt.rs

Created May 11, 2025 18:26

Finds the ceiling value of square root with Rust.

	/// Finds the ceiling value of square root of `n`.
	pub fn ceil_sqrt(n: i64) -> i64 {
	let mut base = (n as f64).sqrt() as i64 - 1;
	while (base + 1) * (base + 1) <= n {
	base += 1;
	}
	base
	}

MikuroXina / parser.hs

Last active April 28, 2025 15:30

An implementation of parser combinator with Haskell.

	{-# LANGUAGE LambdaCase #-}
	{-# OPTIONS_GHC -Wno-name-shadowing #-}

	module Lib (
	(+++),
	chainL,
	chainR,
	char,
	delimited,
	integer,

Mikuroさいな MikuroXina