This file contains hidden or 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 dne_iff_lem : | |
| (∀p : Prop, ¬¬p -> p) ↔ (∀p: Prop, p ∨ ¬p) := by | |
| unfold Not | |
| constructor | |
| · intros dne q | |
| apply dne | |
| intros h0 | |
| apply h0 | |
| right | |
| intros hq |
This file contains hidden or 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 dne_then_lem : (forall (P: Prop), (~~P -> P)) -> (forall (Q: Prop),(Q \/ ~Q)). | |
| Proof. | |
| unfold not. | |
| intros. | |
| apply H. | |
| intros. | |
| apply H0. | |
| right. | |
| intros. | |
| apply H0. |
This file contains hidden or 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
| import "list" | |
| #floors: { | |
| for i in list.Range(0, 1000, 1) { | |
| "floor\(i)": { | |
| for j in list.Range(i, i+100, 1) { | |
| "\(j)": string | |
| } | |
| } | |
| } |
This file contains hidden or 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
| ops(+). | |
| ops(-). | |
| ops(*). | |
| ops(/). | |
| calc([], [Result], Result). | |
| calc([+ | Rest], [B, A | Stack], Result) :- calc(Rest, [A + B | Stack], Result). | |
| calc([- | Rest], [B, A | Stack], Result) :- calc(Rest, [A - B | Stack], Result). | |
| calc([- | Rest], [B, A | Stack], Result) :- calc(Rest, [B - A | Stack], Result). | |
| calc([* | Rest], [B, A | Stack], Result) :- calc(Rest, [A * B | Stack], Result). |
This file contains hidden or 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
| :- use_module(library(clpfd)). | |
| :- use_module(library(lists)). | |
| month_rows([ | |
| [[jan, _, _, _, _, _, xxx], [_, _, _, _, _, _, xxx]], | |
| [[_, feb, _, _, _, _, xxx], [_, _, _, _, _, _, xxx]], | |
| [[_, _, mar, _, _, _, xxx], [_, _, _, _, _, _, xxx]], | |
| [[_, _, _, apr, _, _, xxx], [_, _, _, _, _, _, xxx]], | |
| [[_, _, _, _, may, _, xxx], [_, _, _, _, _, _, xxx]], | |
| [[_, _, _, _, _, jun, xxx], [_, _, _, _, _, _, xxx]], |
This file contains hidden or 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
| import std.stdio; | |
| import std.array; | |
| import std.algorithm; | |
| import std.format; | |
| import std.conv; | |
| import std.range; | |
| // gron scrapbox.json | rg 'lines\[' | rg --pcre2 -o '(?<= = ").*\S(?=";)' | sed -e 's/\\t/ /g' -e 's/&/\&/g' -e 's/\\"/\"/g' | ./scrapbox_to_opml | |
| void main() |
This file contains hidden or 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
| (0..9).to_a.repeated_combination(4).each do |fourDigits| | |
| ten = false | |
| first = false | |
| fourDigits.permutation.each do |a, b, c, d| | |
| ['+', '-', '*', '/'].repeated_permutation(3).each do |op1, op2, op3| | |
| term = "((#{a}.0#{op1}#{b}.0)#{op2}#{c}.0)#{op3}#{d}.0" | |
| if (eval(term) == 10.0 rescue false) | |
| ten = true | |
| break | |
| end |
This file contains hidden or 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
| #include <unistd.h> | |
| #include <sys/wait.h> | |
| #include <sys/types.h> | |
| #include <iostream> | |
| #include <fstream> | |
| #include <string> | |
| #include <vector> | |
| #include <boost/interprocess/sync/file_lock.hpp> | |
| #include <boost/interprocess/sync/scoped_lock.hpp> |
This file contains hidden or 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
| const wait = function*(bullet, n) { | |
| for(let i = 0; i < n; ++i) { | |
| bullet = yield { | |
| isChangeScript: false, | |
| changedBullet: bullet, | |
| newBullets: [], | |
| }; | |
| } | |
| return bullet; |
This file contains hidden or 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
| import std.stdio : writeln; | |
| import std.range : iota; | |
| import std.array : array; | |
| import std.algorithm : fold, nextPermutation, all, sort; | |
| import std.typecons : tuple, Tuple; | |
| import std.parallelism : parallel; | |
| enum MAX = 20; | |
| bool isPrime(in int n){ |
NewerOlder