Skip to content

Instantly share code, notes, and snippets.

View ChAoSUnItY's full-sized avatar
:fishsticks:
Ars Longa Vita Brevis

Kyle Lin ChAoSUnItY

:fishsticks:
Ars Longa Vita Brevis
View GitHub Profile
@ChAoSUnItY
ChAoSUnItY / list-rotate.agda
Created December 13, 2024 16:49
List rotation algorithm equality proof
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl; cong; subst; sym; cong-app)
open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎)
open import Data.List using (List; _∷_; []; _++_; take; drop)
open import Data.List.Properties using (++-identityʳ; ++-assoc)
reverse : ∀ {A : Set} → List A → List A
reverse [] = []
reverse (x ∷ xs) = reverse xs ++ (x ∷ [])
@ChAoSUnItY
ChAoSUnItY / rule110.scala
Last active August 27, 2024 08:45
Scala 3 Type Level Rule110 Implementation (Manual Induction Definition Approach)
import org.tpolecat.typename.*
import scala.annotation.nowarn
import scala.util.matching.Regex
sealed trait Nat
class Zero extends Nat
class Suc[N <: Nat] extends Zero
type _0 = Zero
@ChAoSUnItY
ChAoSUnItY / rule110.scala
Last active August 27, 2024 11:22
Scala 3 Type Level Rule110 Implementation
import org.tpolecat.typename._
sealed trait Nat
class Zero extends Nat
class Suc[N <: Nat] extends Zero
type _0 = Zero
type _1 = Suc[_0]
type _2 = Suc[_1]
@ChAoSUnItY
ChAoSUnItY / typeLevelVector.scala
Last active August 26, 2024 06:50
Scala 3 Type Level Vector (Indexed Data Type)
import org.tpolecat.typename._
sealed trait Nat
class Zero extends Nat
class Suc[N <: Nat] extends Zero
type _0 = Zero
type _1 = Suc[_0]
sealed trait Vec[+T] {
@ChAoSUnItY
ChAoSUnItY / d2.txt
Last active December 2, 2023 08:49
AoC 2023 2-1
Game 1: 1 red, 5 blue, 1 green; 16 blue, 3 red; 6 blue, 5 red; 4 red, 7 blue, 1 green
Game 2: 4 blue; 4 red, 3 blue, 1 green; 4 red, 9 blue, 2 green; 5 blue, 7 green, 4 red
Game 3: 10 blue; 7 blue, 1 green; 19 blue, 1 green, 9 red
Game 4: 2 green; 14 blue, 14 red, 4 green; 12 red, 11 green, 13 blue; 5 green, 9 red, 4 blue; 9 red, 7 green, 12 blue; 2 green, 3 blue, 8 red
Game 5: 3 blue, 4 red; 12 red, 2 green, 15 blue; 1 red, 10 blue, 1 green
Game 6: 1 blue, 7 red; 3 green, 5 red, 1 blue; 1 green, 7 red; 6 red, 1 blue, 4 green; 1 green, 8 red, 1 blue; 2 green, 4 red, 1 blue
Game 7: 11 green, 10 blue, 2 red; 1 green, 12 blue, 2 red; 9 green, 14 blue; 1 red, 19 blue, 15 green
Game 8: 4 green, 2 red, 14 blue; 9 green, 1 red, 15 blue; 2 green, 9 red, 8 blue; 11 green, 7 red, 8 blue; 9 red, 7 green, 6 blue
Game 9: 4 blue, 1 green, 2 red; 1 blue, 3 red; 1 red, 3 blue, 3 green
Game 10: 4 red, 3 green, 6 blue; 2 green, 15 blue, 6 red; 3 green, 2 blue; 2 red, 1 green; 11 blue, 7 red, 4 green; 2 blue, 2 red, 4 green
@ChAoSUnItY
ChAoSUnItY / BigInt.cpp
Created October 27, 2023 07:57
BigInt DS
#include <iostream>
#include <string>
#include <time.h>
#define MAX 40
#define ADD_SUB 19
using namespace std;
struct LongInt
@ChAoSUnItY
ChAoSUnItY / Settings.DotSettings
Created January 2, 2023 12:55
My Rider setting
<wpf:ResourceDictionary xml:space="preserve" xmlns:x="http://schemas.microsoft.com/winfx/2006/xaml" xmlns:s="clr-namespace:System;assembly=mscorlib" xmlns:ss="urn:shemas-jetbrains-com:settings-storage-xaml" xmlns:wpf="http://schemas.microsoft.com/winfx/2006/xaml/presentation">
<s:Boolean x:Key="/Default/CodeStyle/CodeFormatting/CSharpFormat/ALIGN_FIRST_ARG_BY_PAREN/@EntryValue">True</s:Boolean>
<s:Boolean x:Key="/Default/CodeStyle/CodeFormatting/CSharpFormat/ALIGN_LINQ_QUERY/@EntryValue">True</s:Boolean>
<s:Boolean x:Key="/Default/CodeStyle/CodeFormatting/CSharpFormat/ALIGN_MULTILINE_ARGUMENT/@EntryValue">True</s:Boolean>
<s:Boolean x:Key="/Default/CodeStyle/CodeFormatting/CSharpFormat/ALIGN_MULTILINE_CALLS_CHAIN/@EntryValue">True</s:Boolean>
<s:Boolean x:Key="/Default/CodeStyle/CodeFormatting/CSharpFormat/ALIGN_MULTILINE_EXTENDS_LIST/@EntryValue">True</s:Boolean>
<s:Boolean x:Key="/Default/CodeStyle/CodeFormatting/CSharpFormat/ALIGN_MULTILINE_PARAMETER/@EntryValue">True</s:Boolean>
<s:Boolean x:Key="/
@ChAoSUnItY
ChAoSUnItY / Lang2Json.js
Created July 19, 2021 07:09
BigBrainMoment
const fs = require("fs")
const readline = require('readline')
async function processLineByLine() {
const fileStream = fs.createReadStream('mc.lang');
const rl = readline.createInterface({
input: fileStream,
crlfDelay: Infinity
});
@ChAoSUnItY
ChAoSUnItY / Main.java
Last active December 22, 2020 06:26
小論文實驗源代碼
import java.io.FileWriter;
import java.io.IOException;
import java.util.Arrays;
public class Main {
int fib(int n) {
if (n == 0 || n == 1)
return n;
return fib(n - 1) + fib(n - 2);
}
package test;
import java.util.Arrays;
import java.util.Scanner;
public class Main {
public static void main(String[] args) {
Scanner in = new Scanner(System.in);
while (in.hasNext()) {
int ownerWins = 0, guestWin = 0;