зеркало из
https://github.com/iharh/notes.git
synced 2025-10-29 20:56:06 +02:00
25 строки
583 B
Plaintext
25 строки
583 B
Plaintext
Term Format
|
|
http://maxim.livejournal.com/464619.html
|
|
|
|
https://leanprover-community.github.io/learn.html
|
|
|
|
https://github.com/digama0/lean-type-theory
|
|
|
|
Presentations:
|
|
|
|
DeMoura
|
|
http://www.cs.cmu.edu/~soonhok/talks/20131004/#/
|
|
|
|
-- We need UIP, K-axiom of proof irrelevance
|
|
|
|
https://loogle.lean-lang.org/
|
|
https://github.com/nomeata/loogle
|
|
|
|
https://leanprover-community.github.io/mathlib4_docs/
|
|
https://github.com/leanprover-community/mathlib4
|
|
|
|
2021
|
|
Artem Vasilyev - Lean
|
|
https://www.youtube.com/playlist?list=PLlVmvffm-nlI8F9uiZ62pFyzjLvOkkYLU
|
|
https://github.com/vartem/lean-itmo
|