{{ message }}

Instantly share code, notes, and snippets.

💭
I may be slow to respond.

# Kuniwak Kuniwak

💭
I may be slow to respond.
Created Jul 15, 2022
View Well_Not_Dense_Order.thy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 theory "Well_Not_Dense_Order" imports Main begin context wellorder begin definition bot :: 'a where "bot ≡ LEAST x. True" sublocale order_bot bot less_eq less proof standard fix a
Created Jul 15, 2022

View Well_Dense_Order.thy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 theory "Well_Dense_Order" imports Main begin datatype a = A text "a は整列順序である。" instantiation a :: wellorder begin definition less_eq_a :: "a ⇒ a ⇒ bool" where "less_eq_a a b ≡ True"
Last active Aug 28, 2021
View FiniteSet_fold.thy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 theorem fixes f :: "'x ⇒ 'y ⇒ 'y" assumes finite: "finite X" and eq: "⋀x. x ∈ X ⟹ f x = g x" shows "Finite_Set.fold f z X = Finite_Set.fold g z X" using finite using eq by (rule_tac fold_closed_eq[where ?B=UNIV]; simp)
Created Jul 21, 2019
View build-logs.md

# Before

```\$ sw_vers
ProductName:	Mac OS X
ProductVersion:	10.14.5
BuildVersion:	18F132

\$ xcodebuild -version
Xcode 10.2.1```
Created Jul 18, 2019
View longer-timeout.patch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 --- appium-base-driver/lib/express/server.js 2019-07-17 12:37:19.000000000 +0900 +++ appium-base-driver/lib/express/server.js 2019-07-17 12:37:49.000000000 +0900 @@ -49,7 +49,7 @@ async function server (configureRoutes, reject(err); }); httpServer.on('connection', (socket) => { - socket.setTimeout(600 * 1000); // 10 minute timeout + socket.setTimeout(600 * 10000); // 10 minute timeout socket.on('error', reject); });
Last active May 27, 2019

View 1-playground.tla
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 ----------------------------- MODULE playground ----------------------------- VARIABLES varTable \* Initial Predicate: Init == varTable = { <<0, "a">>, <<1, "b">> } \* Next-state relation: Next == varTable' = { <<2, "c">> }
Last active Mar 2, 2019
View stupid_verification_approach.md

# やりたいこと

GUI アプリケーションのドメインを、小さなステートマシンの協調として表現しようとすると、頻繁にバグる上に単体テストの入力空間が手書きするにはでかくて、適切なサンプルを選ぶのも作るのもだるい。そこで、コードのアノテーションから状態機械のモデルを作って性質を証明するようにできたら、結構楽になる。

# 疑問

このように、別言語のアノテーションで状態機械のモデルをつくるアプローチをほとんど知らないのだが、既存でそういうのあるだろうか。

# 超雑な例

Created Feb 28, 2019
Useful xcconfig for SwiftSyntax
View Config.xcconfig
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 CUSTOM_SWIFT_SOURCE = \$(SRCROOT)/path/to/swift-source HEADER_SEARCH_PATHS = \$(CUSTOM_SWIFT_SOURCE)/swift/include/swift-c/SyntaxParser LIBRARY_SEARCH_PATHS = \$(CUSTOM_SWIFT_SOURCE)/build/Ninja-RelWithDebInfoAssert/swift-macosx-x86_64/lib LD_RUNPATH_SEARCH_PATHS = \$(LIBRARY_SEARCH_PATHS)
Created Dec 16, 2018
View typescript-inferring.ts
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 class A { a: "a" = "a"; } class B { b: "b" = "b"; } interface X { a: Y; b: Y; } interface Y { t: T; } type Z = { [key in "a"]: Y };
Created Oct 19, 2018
View Result.swift
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 public enum Result { case success(T) case failure(because: E) public var isSuccess: Bool { switch self { case .success: return true case .failure: