Create accountLogin

Recent searches

No recent searches

Search options

Not available on functional.cafe.
functional.cafe is one of the many independent Mastodon servers you can use to participate in the fediverse.
functional.cafe is an instance for people interested in functional programming and languages.

Administered by:

Server stats:

217
active users

functional.cafe: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.0-alpha.4+glitch

Public

@kha IIRC, very roughly: people didn't love the ML modules (which I guess Lean avoids?), and preferred a command to attach bodies to axioms, but we never finalized a design. I can find discussions later...

Independently, I've linked your Q on our Zulip — I'll try to take a closer look later!

Public

@Blaisorblade Thanks! Attaching the bodies separately is an interesting idea. For Lean indeed I would like to go in a different direction, generating the interface file from the full file but with more flexibility than .vos (and only one pass).

Public

@kha Oh, since Lean avoids typical ambiguity,
single-pass vos in Lean becomes easy, isn't it?

Is the extra flexibility about hiding bodies, and does that interact with arxiv.org/abs/2210.05420 ?

arXiv.orgControlling unfolding in type theoryWe present a novel mechanism for controlling the unfolding of definitions in dependent type theory. Traditionally, proof assistants let users specify whether each definition can or cannot be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core type theory with extension types, a connective first introduced in the context of homotopy type theory. We prove a normalization theorem for our core calculus and have implemented our system in the cooltt proof assistant, providing both theoretical and practical evidence for it.
Public

@Blaisorblade Yes, there is no need for a global step. We do have some leaks from proof bodies but people seem to agree that these should be fixed anyway.

Controlling unfolding across files will be a big part of it, yes, controlling it inside a file would be a nice but somewhat orthogonal extension I think (and needs to interact with caches :/).

I wrote down some musings on the future of Lean's module system in leanprover.github.io/papers/th

Public

@kha @Blaisorblade exciting!

Public

@kha I've added github.com/coq/ceps/pull/62#is my high-level questions about `Link A_body with A_parameter.`

GitHubSeparate compilation by gmalecha · Pull Request #62 · coq/cepsBy gmalecha
Public

@Blaisorblade @kha I think I have seen Gaetan Gilbert grumble that the module system is a mess.

Public

@kha Also, thanks for the interest and curious about the "unsuccessful tries" — is there sth we could/should improve?

Public

@Blaisorblade The terminology around this topic is certainly confusing, I must have picked the wrong combinations for googling. Always hard to search for something you don't know whether it exists!

Public

@Blaisorblade The PA.SE post was my try at having others do that work for me :>

ExploreLive feeds
About