Hypatia du Bois-Marie 形式科學為人權 中共下台 analytic-bias
🏴
analytic-bias
/ embed_video.tex
Created
April 2, 2025 04:46
— forked from FedericoTartarini/embed_video.tex
Embed a video into LaTeX wihout using Flash
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
| %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| % this code was copied from https://tex.stackexchange.com/a/516102 | |
| %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| \usepackage[bigfiles]{pdfbase} | |
| \ExplSyntaxOn | |
| \NewDocumentCommand\embedvideo{smm}{ | |
| \group_begin: | |
| \leavevmode | |
| \tl_if_exist:cTF{file_\file_mdfive_hash:n{#3}}{ |
analytic-bias
/ main.agda
Last active
October 23, 2023 10:46
— forked from wenkokke/main.agda
Code extracted from "Formalising type-logical grammars in Agda".
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
| -- This file contains the code from the paper "Formalising | |
| -- type-logical grammars in Agda", and was directly extracted from the | |
| -- paper's source. | |
| -- | |
| -- Note: because the symbol customarily used for the "left difference" | |
| -- is unavailable in the Unicode character set, and the backslash used | |
| -- for implication is often a reserved symbol, the source file uses a | |
| -- different notation for the connectives: the left and right | |
| -- implications are represented by the double arrows "⇐" and "⇒", and |