まず、以前のLeanを削除する。 elan self uninstall vscodeが上がってたいので、プロセスが使われている云々のエラーが出たが、アンインストールはされた。 https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 を何でもいいからgetし…

A Graphical User Interface Framework for Formal Verification https://drops.dagstuhl.de/opus/volltexte/2021/13899/pdf/LIPIcs-ITP-2021-4.pdf Design of point-and-click user interfaces for proof assistants https://www.chimaira.org/archive/ICFE…

テレスコープの起源は テレスコープ - (新) 檜山正幸のキマイラ飼育記 メモ編 。依存ペアの一般化である依存タプルを定義する。テレスコピックファミリーとは、ファミリーの系列 $`F_0, F_1, \cdots F_n`$ で、次を満たすもの。$`\mathrm{dom}(F_i) = I_i`$ …

Title: Telescopic mappings in typed lambda calculus Author: N.G. de Bruijn Date: 1991 URL: https://www.win.tue.nl/automath/archive/pdf/aut103.pdf In Automath (see [I] ,[3] ,[4]) the implementation of mathematical functions is a simple matt…

CommonJS方式 exports と module.exports - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。CJSエクスポートのエミュレート - (新) 檜山正幸のキマイラ飼育記 メモ編 とも関係する。https://jovi0608.hatenablog.com/entry/20111226/1324879536 に書いてある…

https://www.youtube.com/watch?v=kQIloPijGaw でメレイロ〈Juan F. Meleiro〉が、collective（名詞）とcollectivization（動詞からの名詞）を使っていた。動詞 collectiviz は全然違った意味があるようだ。コレクティビゼーションは、包括原理の構造版で、…