类型系统高阶归纳类型类型理论实数CoqIdrisAgda代数拓扑同伦论

用类型系统描述实数的精髓是什么?

Colliot4 months ago

有多种做法,精髓在于描述出来的实数能符合实数的很多性质,比如实数的完备性。

ice10004 months ago

Preview:

Cancel

Elsewhere

YangKeao replied to 关于树、图的排版算法,现在做到什么程度了?

啥叫完备?啥叫随心所欲?我感觉graphviz还非常原始(或者说不智能),在很多时候我会选择自己手动指定座标。

Colliot replied to 一个重大的消息——本站的 Angular 版本不再继续开发,将会用 React 「重新」开发

Angular 作为一个框架,限制很多。特别是它的编译工具,你随便搞一个组件不引用(比如只在 storybook 中用到),它生产模式 AOT 的时候都会报说,你没有在某个模块里引用这个组件。 在 storybook 里,它只能这么写: .add( 'Registration Dialog', () => ({ component: LogindialogComponent, moduleMetadata: { imports: [HttpModule, RouterTestingModule], schemas: [], declarations: [AppLeftNavTopComponent, AppLeftNavBottomComponent], providers: [], }, props: { resources: resources.zh, language: 'Chinese', dialogShow: true, }, }), ) 这时候不能根据 component 的定义对 props 进行类型检查——它的 props 是用 @Input() public someProp: boolean = false; 这样的带有 decorator 的类属性的语法定义的。 另外,如果你想搞 parent 组件(比如在 storybook 中用一个容器包裹住你的组件,当然也可以不在 storybook 中),如果是 React,你可以简单地这么写: return <div style={{height: 500}}> <YourChildComponent /> /div> 但是在 Angular 里,居然是无法实现类似的效果的。Angular 的视图依赖的是模板,但你也无法像 Vue 那样简便地用一个有 template 字段的对象定义一个组件,而必须用一个类。这样就回到了之前的问题,AOT 的时候会报这个类没有被引用…… 实际上它可以通过 NgComponentOutlet 实现动态渲染一个组件,但是这个时候传 props 变得非常麻烦。我看见的解决方案都是在 child 组件的构造函数里注入这些参数的(因为这个 NgComponentOutlet 只能提供这样的 API),非常地反人类。

YangKeao replied to 一篇不错的关于代理的文章

redsocks 现已原生支持 ss。 Wireguard 非常好用,资源消耗远小于 OpenVPN (甚至远小于关闭全部加密的 OpenVPN )

Colliot replied to 为什么 Realtek 8821ae 网卡在 Ubuntu 下特别慢?

同一台机器,重启到 Windows,网络就是正常水平,所以应该不是硬件坏了或者天线被干扰了……

Colliot replied to macOS 内核扩展的开发,看起来很有意思啊!

话说这个页面打开好快啊,不知道是不是因为缓存了……

Colliot replied to 如何获取一个网站的所有「人性化」的 Bug 列表?

发现一个 BUG,当一个 tag 为 active 状态的时候,它的 margin-right 会消失。

Colliot replied to 这个关于改进 CLI 工具体验的文章不错

第一个 bat 是 Rust 写的啊,简直好评!

Colliot replied to 为森么注册取名至少五个字符

可能是为了模仿 QQ 号的长度限制。短的 ID 可能作为 VIP ID……

Home

Babel

Knowledge

Epistemology

Settings