我这种非网络安全系的弱智都能弄到几 k 电话号码，可惜现在各种底层的东西防护做得比较到位了软件健壮性漏洞也不容易出了，应用层真是喜事连连，唉…

#net #recommended #tools https://github.com/jagt/clumsy

这个工具可以用来模拟网络稳定性状态环境，一般无法做到『优化』，但可以让环境变得更差

#unix #tools #recommended https://github.com/sharkdp/bat

果不其然是 #Rust 程序员设计的，他们最会搞这种扩展版本的 UNIX 系统工具了
也只有 Rust 程序员这么有设计和包装觉悟，而且还有能力开发这种有点算法和底层知识要求的项目

https://zh.wikipedia.org/wiki/%E4%BE%9D%E8%B5%96%E7%B1%BB%E5%9E%8B

https://www.idris-lang.org/

https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html#introduction-to-agda

这 Dependent Type 的资料，不过我这次是<del>伸手</del>问了... 虽然没几个知乎大佬有能耐答这类玩意，因为其实我还是很喜欢这些类型数理逻辑理论的，虽然我目前基本函数式也不是太会，由此看来其实 wikipedia 大佬们是蛮厉害了，各种 CS 理论都有翻译，好耶。

USTC 学生弄的那 Type safe printf 被喷是垃圾（或者是我弄的东西被喷是垃圾），不过我也觉得是垃圾就是了...
因为这个例子看起来就是伪代码一样的，也编译不过...

#PLT #CS #learn #Agda duangsuse 来和你们说一下目前学到很简单很简单很基础很基础的逻辑类的知识，下面的都是 Unicode 表示，不是 TeX

= 这些是 Java、Ruby、Kotlin 程序员们能用到的部分 =

是什么呢？就是 Any#equals（相等性判断）要满足的基本属性，现在一些不 trivial 的 JVM 工程书本上都有教。

我们假设下面的代码示例都有 val a = Any() 的环境

+ 自反性（reflexive）

a.equals(a) 只要 a 不是 null（当然，Kotlin 里 Any 容器的取值不可能是 null），就应该返回 true

数学公式 ∀x. x R x （TeX 代码 \forall x . x \mathrel{R} x ）

+ 对称性（symmetric）

假设有一个对象 b.equals(a) == true 那么，a.equals(b) 也应该为 true

数学公式 a R b → b R a

+ 传递性（transitive）

假设有对象 b.equals(a) == true, c.equals(b) == true 那么，a.equals(c) 也应该为 true

数学公式 a R b → b R c → a R c

btw. 面向计算机科学的偏序理论里，集合 X 上的二元关系 ⊑ 同时满足自反性和传递性时被称作一个前序（Preorder）

btw. 偏序理论里，前序只需要再满足反对称即可成为一个偏序（PartialOrder）
反对称（antisymmetric）的公式是 a R b → b R a → a = b
就是说，a R b 对称蕴含 a 就是 b 这种理论，举个例子，数学上的 + 是对称的，数学上的 - 是反对称的（可能吧）

+ 一致性（consistent）

就是说如果参数（包括调用接受者本身，就是说 this）相同，不管调用多少次 equals 都获得相同的结果，就是说它的数据输入输出流全是显式的，是纯函数。

IDEA 现在能给你实现的 equals 函数推荐这个 pure contract 就是这个意思

= 下面的不保证是有用的 =

btw. 我找到了一个中文名字的计算机科学程序设计语言理论的教授，现在国内根本找不到他的资料，你们听说过吗？

http://www.cs.rhul.ac.uk/~zhaohui/ 这个好像是姓罗的 professor

https://zh.wikipedia.org/wiki/Agda#cite_note-3 — 从这里看到的，弄的啥 UTT （Unified Theory of Dependent Types）

他这本 Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science

现在还在收 PhD 学生你们要不要去啊（逃，跟你们开个玩笑，因为我知道本频道没有正好要留学并且对 PL 感兴趣的

《CLR via C#》、《Kotlin 极简教程》这些书上有讲。其实有时候发现这些玩意还是蛮好玩的，只要理解不出问题就可以
而且又能增长见识，如果有时间，看看这些东西，多好。
然后我又单单发了这些偏序理论，函数式的基本理论懒得发了，其实有些东西还是要自己看书，不好理解就多看几遍，没人能替你理解。

所以我最后看了一个上午就会写这一点破烂 Agda 代码，都是 refl(ective) 的相关证明，就是那种即得易见平凡都算不上的那种

我也不知道是背下来的还是学下来的（笑），但我相信即使现在只是背下来以后也真的能学出来（

顺推冰封专门给 Agda 入门写的书 《好耶，是形式验证！》 （可惜他写了你们也没人看，你们非常满足于自己平时所写的那一点写出来立即就能体验到日常使用他们快感的『源于生活去向生活』前端应用和 Web 后端，笑）

btw. 自豪地，我也有能力写书，不过我之前写的那 Ruby 入门的确是 LibreOffice 排版的，有点不像书。其实 TeX 这玩意也蛮好玩的，中文排版也做得，虽然我不会自定义命令但还能用

data _≡_ : {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x

_≡_ refl refl = refl

{- 下面是对称性 a R b → b R a -}
symm : ∀ {a b} {A : Set a} {B : Set b} → (a → b) → (b → a)

{- 下面是传递性 -}
trans : ∀ {A : Set} {a b c : A} → (a → b) → (b → c) → (a → c)

{- 下面是 Functor -}
⋙ : {a b} {A : Set a} {B : Set b} (f : A → B) {m n} → m ≡ n → f m ≡ f n

如果写错了 Agda 不 check 过就算了，反正我也是弱子状态
with 语法、类型构造器语法、类型签名、Coinductive data types GADT、充要条件、dot pattern、rewrite 什么的暂时忘记或者没学会，因为有些概念我得猜... 是猜啊，有时候形式化定义也不好理解的... 反正需要时间，有误解随便喷吧。不说了

顺便借着这类『静态证明程序正确性』的广播再讲个笔记，是关于预测未来是否能实现的 #file #life #science #PL #CS

我也看过一本和『时间操控』有关的小说，和另一部有名的电影：《时间深渊》和《星际穿越》（btw. 就是著名『墨菲定律』的出处，我开始不记得这名字了然后 科幻电影 女儿 木星 常数 时间 几个关键字一查居然知乎专栏找出来了）

顺便推荐 #book 时间废墟，这么随便乱搞时间，其实是暴露人性相关的也很好看，但是成真了以后未必好玩。

他们都有一个经典的观点，就是四位时空里，『时间』也是一种维度，然后那个维度的生物可以随便操纵时间维，反正就可以理解为我们是鱼肉，他们是刀钜，他们是玩玩偶的人我们是木偶就可以了。

咱们今天就来聊聊时间和人类意识相关的东西，虽然我只有高二的水平... 正好么，反正『不识庐山真面目，只原身在此山中』，<del>100% 的正确率谁也不敢保证，10 分钟你看不了吃亏你看不了上当</del>，无法证实的猜想只能是猜想罢了。正如一个权限受到限制的应用程序也不可能知道 Ring0（内核层）的一些事情（诸如当前的 proccess vector）一样，我们这个受到限制的视角也很难做到什么全知全能。大家开心即可。不管说啥唯物主义啥唯心主义，目前保持好好活着的态度即可。政治和道德人伦理性感性都正确。多好。

为什么听我讲...
1. 我觉得我讲得很接地气你们都听得懂
2. 这是程序员给程序员讲的，灰常适合程序员
3. 你们不觉得程序员是个很厉害的职业么？日常工作之中使用各种高大上充分体现人类智慧的理论
4. 你们闲得没事（对于学生党来说就是说你们因为课业繁忙没有时间写代码但还有时间看小说那种），而且这事情有助于开阔眼界增长见识，虽然可能是我臆想编造出来的

无论你有多聪明，无论你的理论有多完美，如果不符合实际，那么它就是错的
— 物理学家 理查德·费曼（Richard Phillips Feynman）

不过有些东西太难以估测，我们这里不说四维时空这种让 Iterable<Frame> 完全变成 RandomAccess<Frame> 的东西，因为如果真的可以随机访问，理论上四维时空真的是可以操纵一切的，并且不会出类似停机问题这种『确定性问题』

首先咱们还是 <del>两句不离老本行</del> 说说啥是维度

在数学里，维度就是... 好吧我不知道，某度百科说是 独立参数的数目
Wikipedia 是最好的学术交流资料

在物理里维度就是 ::

data class Dimension4<R, T>(var x: R, var y: R, var z: R, var t: T)



import java.util.Date

typealias Dimension<R, T> = Dimension4<R, T>

>>> Dimension<Int, Int>(0, 0, 0, 0)
Dimension(x=0, y=0, z=0, t=0)

>>> Dimension<Int, Date>(0, 0, 0, Date())
Dimension(x=0, y=0, z=0, t=Fri Nov 30 16:00:20 CST 2018)

就是说这是个四维元组（就是有四个项目的匿名结构体 struct），三个是（R 类型的）『空间维』，一个是（T 类型的）『时间维』
当然这种简单的泛型使用其实不算什么技能，可以单纯把泛型当成是一种“类型参数”即可，这里不讲泛型，你们可以假设我往 <R, T> 里填 <Int, Date> 的时候某个 data class 里的 T 类型变成了 Date，R 类型变成了 Int
这里不考虑泛型的协变（Covariant）和逆变（Contravariant）的问题，理解万岁

在生活里，维度就是我们对相对位置的简单抽象，拿各种游戏引擎做 2D、3D 视频游戏的同学们肯定非常了解（当然喽）

type XY = (Int, Int) deriving (Eq, Show) -- 二维
type XYZ = (Int, Int, Int) deriving (Eq, Show) -- 三维
type XYZW = (Int, Int, Int, Int) deriving (Eq, Show) -- 四维

这是一个简单的『抽象维度』，当然不要问我为啥不用泛型（当然我也不知道 #Haskell 里这叫不叫泛型 generics），示例而已

然后是数组了，很多语言，哪怕是很早期的 Fortran（真的是很老了，1953-1957）、Lisp（1956 年的版本）、Basic 都有等价于数组（Array）的数据结构（或许 Lisp 的部分不等价，我听说 Lisp 基本都用的是链表...），一般数组实现是使用物理硬件内存上一块连续的空间的（当然由于某些原因也可能不，不过一般都是，我们称这段连续的地址空间叫『buffer，缓冲器』）

数组的维和元组的维差不多，假设我们有个 int fib_first3[3] = {0, 1, 2};，就可以说这个（全局符号） fib_first3 是 3 维的 int 数组，因为一个 Integer 在 64 位机器上是 8 字节（一字节 8 位，4 字节 32 位，8 字节 64 位），这个数组可能需要分配 8 * 3 = 24 字节的 buffer 来容纳它（一些机器还有字节对齐的要求，要不然可能直接崩坏掉 fault 或者造成速度严重降低，为什么降低可能是数据转送要额外步骤或者缓存问题造成的？）（比如你们常用的 x86 架构上的 CDEF 标准，要求对齐到一个字（4 个字节），而这数组就会浪费掉一个字节）
（看不懂是肯定的，因为我写这个不是为了教你们 C 语言和 C 运行时相关的知识）

而一些语言，诸如 C/C++/Basic/C# 还支持交错数组（jagged array）（就是说数组的数组）（搞 OI 的肯定不陌生“多维数组”这个名词，不过我觉得有点混淆的意思就不用了）

int matrix_dim22[2][2] = {
    {0, 1},
    {1, 0}
  };

printf("%i", matrix_dim22[0][1]); //> 1

不过这就是维嘛... 总之就是一个有序的集合。

下面进入正题之一，预测未来的可能性，然后我们再来说说几个问题。

第一个问题是理发师问题，大家想必都听过
第二个问题是停机问题，想必大家都没听过
第三个问题是外祖母问题，这个大概都听过

总结来说：三个都是悖论（好吧，可能有的不是？

我想说的是这个『确定性问题的否定答案』停机问题

我们知道停机问题在图灵机等价的演算模型（比如 lambda 演算 和生命游戏）上都是不可判定的，在逻辑上根本无法在非 infinity 的时间内得出答案或者从实际出发没有答案 — 等算出结果太阳都没了的那种

在简单幼稚的程序设计语言类型里有种类型被称为 buttom type『底类型』
在 subtyping 里，它是所有类型的子类型，因为这种类型根本不可能有实例，这样没有实例的类型当然就可以作为任何类型的子类型喽，检查不出任何问题

在 Kotlin 里面，这种类型叫 Nothing，和 Unit 不一样， Unit 是一个 object，它只有一个实例，而 Noting 则是一个没有实例的类型
在 Rust 里，这种类型叫 never，就是永远都不可能拿到对应值的意思
在 Java 里，这种类型叫 void（不过 JVM 内部的说法是它不是类型，叫 VoidDescriptor，不过，这里当成类型算了...），此外，Java 里有 Boxed 装箱上的 java.lang.Void 类型，它只可能有一个值 — null，因为你拿不到 void 的实例

当然这类理论最好还是推荐冰封的 Agda 博文看看

比方说，在 Rust 里面我们可以定义一个完全不会返回 _Noreturn 的函数 exit_now，因为此函数在求值时会调用 ::std::process::exit，整个进程都退出了，同一个进程里的代码根本拿不到此函数的值：

fn exit_now() -> ! {
  std::process::exit(0);
}

当然你也可以不把返回值 never 写出来

在 Kotlin 里 throw 表达式也是有返回值的，不过类型是 Nothing，因为抛出异常（求值赋值操作右值 throw RuntimeException("Interrupted!")）的时候整个栈帧都 unwind 了，赋值操作根本没有被实际执行，函数异常终止执行，没有返回值。

val a = throw RuntimeException("Interrupted!")
// error: 'Nothing' property type needs to be specified explicitly

val a: Nothing = throw RuntimeException("Interrupted!")
java.lang.RuntimeException: Interrupted!

println(a)
error: unresolved reference: a

下面这个也一样，REPL 没有打印出 never() 调用的返回值

fun never(): Nothing = throw RuntimeException()

>>> never()
java.lang.RuntimeException
        at .never(Unknown Source)

... 废话一堆... 所以这部分简单的道理完了，我们看看下面的：
我们知道，顺序模型里面（相对的就是某电影里外星人的『一目了然』模型，从最开始一生会怎样度过会得什么病什么时候死都知道了）

于是觉得这种观点颇为不妥的我就想办法，虽然可能是抽象层次（或者说，粒度）的问题导致观点不同
于是我写了这些代码（貌似是 Scheme，因为我觉得 Clojure 语法设计有点简洁的过分了，看起来真是烧脑得很）

(define get-the-future (lambda
  ; ...
  (determine-action (get-the-future))))

; 当然你也可以 (define determine-action real-resolve)
(define determine-action (lambda (the-future)
  (real-resolve the-future)))

我们不管什么 partial 不 partial 的问题了（指 real-resolve）
这段代码描述的其实就是『预料未来』带来的一个令我十分头疼的问题，每次我对其进行模拟仿佛都会看到黑洞一样，我认为未来是基于现在状态的『过去是过去的现在，未来是现在的延续』，对未来的预测将会干扰到你的现在，而未来本身又是依赖于现在的，这样就会在传统的顺序模式里捅出篓子，遭致无限递归的尴尬境况 — 想知道未来，就得知道你知道未来以后的未来，就得知道你知道未来以后的未来以后的未来，就得知道你知道未来以后的未来的未来的未来...

结果是无尽递归，永远没有结果，我们知道 get-the-future 永远不会返回，因为它的值会陷于 (get-the-future) application 和 (determine-action ...) application 的无限循环之中，这是真的永远，你知道 fn eternity() -> ! { eternity(); } 是没有结果的，Anything is possible... except Nothing。

或者说，Anything is possible. Nothing is impossible. hhhhhh.

然后我们再给一些不知道啥是薛定谔的猫的人（e.g. 之前的我自己就是）普及一下量子猫箱『又活又死、观测、判定、坍塌、可能性什么的，我非常理解爱因斯坦上帝不会掷骰子的理论，我相信的当然是宇宙模拟器之类的计算机科学相关的非常泛泛的了解，就是说宇宙都可以被抽象成状态... 只要有一个状态 E 就可以拿到下一个状态，一切规律都是根据状态计算的，都是纯的，怎么可能弄出随机数和 50% 活 50% 死』。

当然，我是懒得再去了解那些理论了，有人讲

最后是人类『灵魂』相关的，我称之为灵魂 State （状态）论，其实这个不只是我一个人的想法，很多包括科幻作家也这么想。

duangsuse 也考虑人们对灵魂的遐想，不过其实人们对人类灵魂猜测中有一点特性是绝对存在的：

灵魂绝对依附于物质存在

其实，我们往字缝里看看，就不难看出一个更高层的抽象：

灵魂 S 肯定是 Identifible, Unique （可识别（可以判断其同一性）并且唯一）的，然后为了方便接下来的讨论我们称物质层面的相等性为全等性（===）

我们至少是高二我目前学到的物理没有告诉我们『物质和能量如何互相转化』
其实我不知道『物质』本身是不是 Identifible 的，我不知道能量转化为物质后是不是之前变成能量形式的物质还是新的物质，是不是可重复的（幂等）的
如果灵魂真的是依附物质存在，并且有一种方法可以使物质被毁灭（觉得这里翻译为 drain 比较好？还是 destory？湮灭 annihilation？）并且无法拿到相等的物质，那就可以说灵魂可以被凄惨地毁灭永世不得... 超生 🙈

~~E = mc²~~是原罪，不过照大的探索出的宇宙规律来说一切都是向着最终的死寂走的，所以说看起来，不好玩。向死而生嘛。

不过我不赞同这种说法，因为我考虑了一些别的情况。

首先这是不规范的说法，我觉得物质都是按基本粒子来度量的，这理论非常空洞，没有说灵魂是附着再多大的粒子集合上的。他们考虑的可能就是一层能给人视听等五感的抽象，不过我认为感觉都是假造的，怎么假造我不清楚，得看脑科学。反正就是不实际存在（现在我还喜欢拿这个本来不存在的理论揶揄我自己，然而，造成了不好的副作用，当我没有啥感觉只有思维的时候突然感觉这身体只是一眼线而已，它只不过代表我... （而我不是依附于物质而存...））

其次就是如果是依附于某种特殊物质上，那最开始给那些要出生的小孩子们准备的物质是哪里来的，不要和我扯戒色吧那套伪科学。

当然量子物理上也有人弄出个什么意识子之类的，不过也是一样的理论。我上面说不喜欢这种理论（当然不是为了强行把死人说活，
我经常想着有没有可能死而复生的，所谓天堂会不会就是后来的人类们给先人们造的虚拟环境，虽然可能终究还是随着宇宙的『流动』停止而停止
不是我贪生... 或者说还真有点，求生欲现代中国社会哪个正常人不应该有
然后我就大肆批评我自己，说还真是给你这个欲望了，死去元知万事空，就为了这点 naive 的动物性玩意就破坏所理解的现实，是不好的。给你了求生欲，你就不想死，可是如果不给你呢？如果你是《某科学的超电磁炮 S》 里的『妹妹们』呢？你真的以为你就有那么厉害么？正常的理解只应该为别人考虑，因为自己已经不应该再强求什么，一切都只会返回 Never 了，其实没有求生欲也没什么
或者说，曾经是已经死了的，物质也总是在更新，不会为『死』的自己悲伤
当时就非常为之一振，准确的说是为之一颤... 不知道为什么，但觉得有点难受
并非是开始没有不会自己死自己演替的生命，并非是没有没有求生欲的生命，只不过它们都死了，没有留下来直到现在而已
所以 duangsuse 就想啊，感情上的遗言什么的可以简单一点，首先要告诉我的家人和朋友们让他们开开心心活，然后死后遗体器官能捐则捐，最后追悼会要开喜庆一点
（好吧说远了）

duangsuse 的理论建立是从『替换实验（更准确的说法是猜想）』开始的

现在我们没有把人脑拆为小零件的本事，它自是黑箱不必说

假设未来我们有了呢？假设我们把脑部的一部分替换掉，你还是你吗？

因为有部分物质还是你，所以你可以认为那是你，不过，不是呢？因为替换用的部分完全实现了原来部分的功能，包括『你』的另外一部分在内，谁都无法判断出来你和你有什么区别。

如果实现那部分功能的是各种机器不是生物技术，也是同理。

如果替换掉了 99% 的质量，只有 1% 的质量是『原装』的，你觉得有什么区别？

还是说以 50% 为界呢？还是说有一部分肯定是不能制作出等价替换的呢？因为那部分包含了你的灵魂？又回到了之前灵魂依附于什么粒度的物质的问题了，而我不想管那个问题。你可以选择自己相信或者不信。

或是完全替换掉呢？可对别人来说，你完全就还是你啊？哪怕内部工作方式都变了，但是接口没变，没人能判断得出来。（ps. 这里还有一层抽象，不是状态抽象，是工作方式抽象。我觉得这个理论也很不错。）

于是我们可以就这样不依附物质的理论抽象出状态理论 — 虽然可能是误解，但反正大家现在都是误解（或者没人知道真实的真相），我来参一波也没问题喽

然后就是相等性判断的问题了，既然说什么都是客观的，没有所谓主观你和客观你的区别（虽然可能只是抽象导致的不符合实际），那一些基本操作就可以开始定义了，虽然还涉及到抽象粒度也没有被严谨定义的问题
不过现在考虑这个问题会让理论没法好好讨论... 那物理上能做到完全复刻吗？... 好吧应该不能，物质论是没有这类问题... 可是他们也有别的问题

使用类似 Duck typing 的理论 —
如果一只鸟，走起来像鸭子，叫起来像鸭子，游泳起来也像鸭子，那它就是鸭子。

如果一个人的脑部抽象状态和现在电脑前的 duangsuse 无二，那他就是 duangsuse
其他概念参考箱中之脑

然后我好事又弄了两个问题，就是首先我们有一个 duangsuse，让他停止更新状态（类似麻醉），然后 clone 一份状态和相应物质，使看起来像是有两个主观完全一样的 duangsuse 一样。

然后我们把两个 duangsuse 放在不同的两个地方，同时开始更新状态。问：哪个是最开始的 duangsuse，如果你是最开始还唯一（当然这在状态论里是误区，因为一直只有一个『主观』你）的 duangsuse 你睁开眼睛（如果闭上了）后看到的是场景 1 还是场景 2
... 结果是我自己无法判断，我肯定以为我一直是最开始那个，但这和理论又是相悖的... 现在没时间拿纸算

待解决吧（可以写科幻小说

另一个方面是从所谓『感觉』的量化开始的，夫灵魂如若附依一物而存，则此物重几何？

以前认为疼痛是产生在我们所认为那个部位的，其实从某种意义来说也不为错（切了就好，笑死 hhhhhh）
现在的观点是脑部，包括现在的『箱中之脑』理论，我的观点之前说过，若我就是这箱中之脑也不会为此自杀，正如 #Book 《浮生物语》：一 里『一分为二的金甲神元神』一样，前几世于你这个新状态又有何干？你是你，不是他。

所以这样抽象灵魂，这个量化... 有点不 excited 啊... 因为太多不严谨的东西了

#PL #CS #Zhihu

我的天，你们能不能停止使用容易混淆的表述！Andy 有一大堆，你们说的是哪个 Andy？？？

彭飞 发布了想法：给编译器加新的优化之前需要作什么工作？Andy大神教你做人 https://github.com/dotnet/coreclr/blob/b3475eb87a5f28fb88cf23ebe30f174eff75bb46/Documentation/design-docs/GuardedDevirtualization.md
https://www.zhihu.com/pin/1051685921333886976

这个彭飞大概就是之前和淫王抬杠的那个吧《王垠，请别欺负我们读书少》？我还记得

这个彭飞弄得还是不好，我这里他听不见『背后说人坏话』批评一下

这个 Gist: GuardedDevirtualization.md
是讲 CLR call.virt IL 指令 JIT 分派优化的貌似

因为他这个弄得像 Star 一样，而我是不喜欢对技术这样的态度的（虽然这个文档也的确就是比较早期的一个设计手稿，当然他们也做了执行效率分析什么的），虽然他也是微软的工程师没错，但这个他不写文翻译详细讲就发张图实在是太泛泛了，而且有点标题党的意思。

UPDATE: 弄错了，他标的是 Intel 的编译器工程师

duangsuse 高性能计算现在是比较菜的，不过，loop unrolling、SIMD、Vectorize 矢量化，部分 CPU 做的优化还是知道的，他发或者推荐的东西的确是大部分比较 trivial 的，很多如果看一下认为不干就不看即可，这里也欢迎大佬们来推荐几个编译优化的大佬关注。

#tools #web #oi #recommended

#Ruby https://t.me/dsuset/4528

pry -r convert_data.rb -e 'File.write('res.csv', dump_students.string)' 即可导出所有条目

更新

每次弄这些都很费时间和精力，大概是做少了....

#Learn #TeX
a_{1} \quad x^2 \quad e^{- \alpha t} \quad b^{3}_{ij} \quad e^{2}\neq {e^x}^2
从这抄过来的

复制过来是 a1x2e−αtb3ije2≠ex2

我们从这里能看到 TeX 命令

_i 定义一个下标 i
\quad 是空白方块字符
^n 定义一个上标
\alpha 是希腊字母 alpha
\neq 是不等号
{} 括起来来结合指令如 {e^x}^2

又更新了一下这个无聊的脚本...