因为这个文档真的会有 6 年级小学生来看




我也会这么写。

@Pogbag
@Tink

害搁着犹豫买不买 xbox 呐？ 聪明人 xbox game pass 已经续费到 90 年后了

买不买主机根本不重要，微软爸爸会想办法让所有人都玩到

个人感觉有几样会比较适合：

成人饰品，比如项链，那种得等她 20 几岁戴上才会显得搭配的款式。不太推荐化妆品的原因是这些东西有保质期而且与个人条件有很大关系你不好选。
书，尤其是女性作家写的探讨自身价值观类的书（不过恕我浅薄无法推荐……），我这说的绝不是励志类成功学也不是女拳启蒙更不是当代言情小说，是指比如张爱玲、三毛 这样作家的作品
在有跟随保护的前提下一场「稍有危险性」的旅行（远行、极限运动、「地下场所」，但得匹配你们的家庭教育条件和观念）


尽量不要买「实用性物品」，一来这些东西的符号性和仪式感都太弱，二来容易沦为攀比工具。如果真的「精神素养」不够，那就好好挑挑饰品就行

这个选文件的对话框是「打开文件」对话框？

如果是跟浏览器上传文件时弹的那个「打开文件」一样的东西，那么它在 c#中的用处就仅仅是获取一个文件路径字符串，反编译后改掉逻辑也很简单的。

不过我感觉更科学的方式是直接换掉这个库

我觉得 lz 可能该深刻思考一下
为什么自己会被帖子里很多人习以为常的事情「震碎三观」


另外，那些「不妨碍你写代码」的「学识」
有的是用来避免「别人出口成章，而我只会卧槽」的
有的是用来分辨「这世上存在超自然能量，我的神奇机器包治百病」的
有的是用来驳斥「公司哪里亏待过你了」的


有的是用来
帮助自己思考为什么自己会被很多人习以为常的事情「震碎三观」
的

我又反复看了几遍那篇《蝉语独白》
然后又看了半天英文那版文档……
本来还想直接从单测里找 examples 的但源码里居然没有测试


> We can use check! <exp>: <type>, to make assertion about an expression's type.
看起来「 make assertion 」的含义跟既往理解没什么区别，就是判断一个命题是否正确
但下面的正文里写的意思好像说
「我能为<exp>:<type>下定义」（「我能定义一个<exp>:<type>为真」）
一样。
列举的所有 !check <exp>:<type>我都没看到结论，即断言为真还是假，搞得我一头雾水

--------

然后在「 built-in types 」这章里塞了 Equal ，本来还以为有什么可等性的定义方法，或者可等类型是什么特殊类型
然而似乎也不是
是说 Equal 这个三元组是一个抽象类型？
但是又有一句
> If the two elements are actually not the same, we can still use Equal to create a Type, but we can not construct elements of this type
…………我就搞不懂了如果「 Equal(X,Y,Z)三元组」这个类型是抽象的，那么去哪，谁来判定 Y 和 Z 是不是相等的？能不能 construct 它的实例到底是怎么判定的？

--------

> If Nat is the most basic datatype, List is the next basic datatype.
我猜原意是「如果说自然数算是最基础的类型，那么 List 可以说是第二基础的」
这个 if 就很没逻辑……
然后 List( 这个括号里的参数是一个类型对吧，换言之
List(T)是一个泛型，T 作为构造类型的一部分？
那这样理解的话 Equal()也是一个泛型，List 的参数列表是类型，Equal 里却可以有表达式……为什么？规范是啥……

然后这一节还似乎想讲讲 list 上的归纳法
我 ctrl+f 了一下没看到 return induction ( 这个 induction 函数是哪讲的就放弃了





我的耐心仅够支撑我研究到这，抱歉……
p.s.
话说启发点是 coq ？文档全文也没看出来如何 prove something ，甚至如何定义公理都没讲明白，更别说推导机制……

我看了半天

「断言」的定义

但全文没有讲到「断言有什么用」，语言中也没有与断言相关的语法

首先…………………………

extern 是「外部声明」，它的作用是告诉链接器 (!!) 注意不是编译器，到其它文件去找这个符号。如果 extern 直接放在定义的地方，则是告诉链接器「我这个符号应该让所有地方都能看得到」。

但你这里 extern 只是一个声明。


第二件事，inline 的意义在于告诉编译器 (!!) 注意是编译器，我这个符号的定义可能会重复出现很多次（因为会被 include 到不同文件里去），你就直接把找到的定义照抄放到调用点就行，不用暴露，不会有文件要链接我。




所以你正在试图一边让链接器去找某个符号，一边让编译器不要暴露这个符号以供链接……




「 inline 的非 static 全局函数」是这样的：

a.h
inline void g_f(){}

a.c
#include "a.h"
void a(){g_f();}

b.c
#include "a.h"
void b(){g_f();}

main.c
extern void a();
extern void b();
int main() {a();b();}

翻译一下#13：

「哥几个都吸烟长大的你老几啊说三道四的，不怕走路给你一顿削啊」

你这脚本里双引号套双引号了真的没问题吗……
「输入了不存在的路径」 第一反应是有空格捣乱