V2EX › mizuhashi 的所有回复 › 第 4 页 / 共 5 页

V2EX = way to explore

V2EX 是一个关于分享和探索的地方

现在注册

已注册用户请登录

1 2 3 4 5

❮

❯

2022-06-30 15:23:29 +08:00

agda 的话可以，做法参考 42 楼，你需要构造一个 isTen 类型，然后穿参的时候提供一个这个类型的证明，如果你用 literal 来调用这个证明可以自动产生，但是别的运行时量证明需要你自己写

2022-06-23 22:37:04 +08:00

@kappa 同等难度真不一定有战神 4 容易，砍字幕容易脑溢血

2022-05-21 05:19:49 +08:00

中国的基尼系数要看中南财大的，美国比中国高是不可能的

2022-02-12 12:15:31 +08:00

其实 imba 语言或者说 mithril.js 的状态管理更自然

1 2 3 4 5

❮

❯