lengyijun’s gists

lengyijun / autocd_gitclone.fish

Created January 10, 2025 00:30

auto cd after git clone <url>

	function auto_cd_xdotool --on-event fish_prompt
	if test $status -eq 0
	if string match -q "mkdir*" $history[1]
	set -l splits (string split -n ' ' $history[1])
	for i in $splits[-1..2]
	if not string match -q -- "-*" $i
	xdotool type --delay 100 "cd $i"
	return
	end
	end

lengyijun / weak_Collatz_conjecture_42_3.txt

Created November 14, 2024 00:32

	; https://terrytao.wordpress.com/2011/08/25/the-collatz-conjecture-littlewood-offord-theory-and-powers-of-2-and-3/

	blank_symbol: #
	initial_state: bootstrap_stage_1

	bootstrap_stage_1
	# 1 R bootstrap_stage_2
	0 0 R unreachable
	1 1 R unreachable

lengyijun / weak_Collatz_conjecture_45_3.txt

Created November 13, 2024 00:30

	; https://terrytao.wordpress.com/2011/08/25/the-collatz-conjecture-littlewood-offord-theory-and-powers-of-2-and-3/

	blank_symbol: #
	initial_state: bootstrap_stage_1

	bootstrap_stage_1
	# 1 R cp_stage_5
	0 0 R unreachable
	1 1 R unreachable

lengyijun / list27.txt

Last active October 16, 2024 09:47 — forked from anonymous/list27.txt

lengyijun / dnscrypt-proxy.md

Last active September 22, 2022 02:19 — forked from ndlrx/dnscrypt-proxy.md

Install dnscrypt-proxy on Archlinux or Manjaro

Step 1 - Install and Configure dnscrypt-proxy

sudo su
pacman -S dnscrypt-proxy

cd /etc/dnscrypt-proxy/

lengyijun / learn_record.v

Last active July 15, 2022 11:53

	Require Import
	Coq.FSets.FMapAVL
	Coq.FSets.FMapFacts
	Coq.Structures.OrderedTypeEx
	PeanoNat.

	Module Import M := FMapAVL.Make(Nat_as_OT).
	Print Module M.
	Check (M.t (list nat)).

lengyijun / mergesort.v

Created June 5, 2022 13:55

	Require Export Coq.Lists.List.
	Require Export Coq.Arith.Arith.
	Require Import Program.Wf.

	Program Fixpoint merge (x : list nat) (y : list nat) {measure (length x + length y)} : list nat :=
	match x with
	\| x1 :: xs =>
	match y with
	\| y1 :: ys => if x1 <=? y1
	then x1::(merge xs y)

lengyijun / hello.v

Created May 28, 2022 10:39

try Program Fixpoint

	Require Export Coq.Lists.List.
	Require Export Coq.Arith.Arith.
	Require Import Program.Wf.

	Program Fixpoint merge (x : list nat) (y : list nat) {measure (length x + length y)} : list nat :=
	match x with
	\| x1 :: xs =>
	match y with
	\| y1 :: ys => if x1 <? y1
	then x1::(merge xs y)

lengyijun / mutual-merge.agda

Created April 24, 2022 05:49

	open import Data.String as String using (String; fromList)
	open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _<′_; _≤′_)
	open import Data.Nat.Properties
	open import Data.Bool using (Bool; true; false; if_then_else_)
	open import Data.List hiding (merge; partition)
	open import Data.List.Properties using (map-id; map-compose)
	open import Data.Product using (Σ; Σ-syntax; _,_; proj₁; proj₂; _×_; map)
	open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; map)
	open import Data.Unit using (⊤; tt)
	open import Data.Empty using (⊥; ⊥-elim)

lengyijun / Merge.v

Created April 20, 2022 04:11

recursive induction

	(** * Merge: Merge Sort, With Specification and Proof of Correctness*)

	From VFA Require Import Perm.
	From VFA Require Import Sort.
	From Coq Require Import Recdef. (* needed for [Function] feature *)

	(** Mergesort is a well-known sorting algorithm, normally presented
	as an imperative algorithm on arrays, that has worst-case
	O(n log n) execution time and requires O(n) auxiliary space.

lyj lengyijun