我觉得 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：

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

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

臭直男的跑到产品这边提要求来了（

@source 你…… 在仔细看看？ 我看到的几乎都是讽刺

gdb 配 https://github.com/hugsy/gef

大型项目根本没什么机会直接挂调试器……几乎都在看 core dump 了



建议提供点更详细的信息，平台、项目组织形式（比如你要调 lib 还是 executable ，有没有单测和 mock 等等）

…… 你应该尝试把那 1w 个正则编译到一起去

既然是路由分发，那么这些正则就必然是静态的，你完全可以把时间都放到编译期。
之前做过一些极重规则的东西，数以万计内置规则，我们用了这个
http://www.colm.net/open-source/ragel/

虽然编译要跑一个小时，但是运行快啊（

@Jooooooooo 歪个楼，你以为的高性能是在减少冷分支……实际上写「高性能代码」的人都已经在 probe CPU 的 register file 有多大了

我第一反应是《云图》
但其实我对这电影也不是很满意，有点过于故弄玄虚，叙事结构也没有把它的精神内核表现得很好，有些遗憾

我问两个问题

农村小孩有手机吗？
你手机丢了还能正常上班回家吗？



农村小孩生活完全不受影响，但你麻烦就大了。

开个题外玩笑： 你没必要跟 35 岁后出现的那些天谴科技对着干