TChan – Telegram

TChan

71 subscribers

11 photos

47 files

225 links

atomically newTChan :: IO TChan

Download Telegram

About

Blog

Apps

Platform

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Core.20support.20for.20coinductive.20predicates/with/543924162

Public view of Lean | Zulip team chat

Browse the publicly accessible channels in Lean without logging in.

338 views13:56

#纸 Lean4Lean: Towards a formalized metatheory for the Lean theorem prover https://arxiv.org/abs/2403.14064

https://youtu.be/GOrIMiI2zLA

Mario Carneiro: Lean4Lean: Formalizing the type theory of Lean

Enjoy the videos and music you love, upload original content, and share it all with friends, family, and the world on YouTube.

140 views09:40

The Type Theory of Lean.pdf

150 views04:02

#纸 Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types: Full definitions, lemmas and proofs
https://arxiv.org/pdf/1601.05106

127 viewsedited 12:58

implication_constraints.pdf

#纸 Complete and Decidable Type Inference for GADTs

137 viewsedited 14:00

https://wiki.haskell.org/index.php?title=User%3AMichiexile%2FMATH198

126 views08:28

https://typst.app/blog/2025/typst-0.14/

Typst: Typst 0.14: Now accessible – Typst Blog

Typst 0.14 is out now. With accessibility by default, PDFs as images, character-level justification, and more, it has everything you need to move from draft to...

138 views20:46

#纸 Correct and Complete Type Checking and Certified Erasure for Coq, in Coq
https://inria.hal.science/hal-04077552v3/document

171 views08:43

https://cs-syd.eu/posts/2024-04-20-static-linking-haskell-nix 🤔

Getting your Haskell executable statically linked with Nix

I have been making my products statically linked over the past few days. This post presents why and how to statically link your Haskell executables and collects a mapping from obscure error to unexpected fixes.This work would not have been possible without…

196 views02:09

#纸 Practical Type Inference with Levels
https://dl.acm.org/doi/pdf/10.1145/3729338

195 views07:58

#TIL GHC 9.8 移除了 kind level equality constraints
https://ryanglscott.github.io/2021/08/01/equality-constraints-in-kinds/

GHC curiosities: Equality constraints in kinds - Ryan Scott

188 views00:09

https://tbelaire.ca/posts/coq-index-vs-parameter.html

181 views19:18

https://gitlab.com/explicit-refinement-types/lean4-formalization

Explicit Refinement Types / lean4-formalization · GitLab

A formalization of logical refinement types in Lean 4

162 views07:31

#书 Certified Programming with Dependent Types

153 views00:18

https://typst.app/docs/changelog/0.14.1/

0.14.1 – Typst Documentation

Changes in Typst 0.14.1

164 views20:51

#纸 Simplifying Casts and Coercions
https://lean-forward.github.io/norm_cast/norm_cast.pdf

163 views08:02

https://typst.app/docs/changelog/0.14.2/

0.14.2 – Typst Documentation

Changes in Typst 0.14.2

181 views18:08

https://www.stephendiehl.com/posts/diaconescu/

Diaconescu's Theorem - Stephen Diehl

Personal blog of Stephen Diehl - Software engineer writing about technology, programming, and the future

147 views22:42

https://leanprover-community.github.io/archive/stream/113488-general/topic/What.20is.20the.20subject.20reduction.20debate.3F.html 🤔

leanprover-community.github.io

Zulip Chat Archive

The homepage for the mathlib library for the Lean theorem prover. Contains an archive of the Zulip chat for discussions about Lean and mathlib.

190 viewsedited 09:23

Forwarded from 喵喵小喵喵 (Meow-meow 🍓)

Don't fall into the anti-AI hype
https://antirez.com/news/158

146 views23:35

#纸 All Your Base Are Belong to Us
https://pleiad.cl/papers/2025/poiretAl-popl2025.pdf

149 views08:30