Top new questions this week:
|
|
In dl.acm.org/doi/10.1145/3290316 section 4 (which I believe is a standard reference), the authors claimed that Voevodsky’s propositional resizing rule justifies the consistency of an …
|
|
So I’m working on type checking of an expression that pattern matches on terms, like case x of in Haskell. My question is, suppose we have …
|
|
I have a hunch I need to figure out versions of unique choice or definite description for partial and multi-valued functions. But I’m entirely confused about how you’d axiomize partial or multi-valued …
|
|
I’m using Lean 4 along with Mathlib. I’m trying to work with lists, but I can’t find a function which obtains the nth entry of a list. It seems pretty hard to find for the most basic function of a …
|
Greatest hits from previous weeks:
|
|
I was looking at the MSC2020 database and I find it hard to identify a field suitable for works about proof assistants and formalised mathematics. 03B70 (“Logic in Computer Science”) might …
|
|
I’m reading Girard’s Proofs and Types, and in section 4.4 he writes: Lemma: t is strongly normalisable iff there is a number …
|
|
I’ve been playing with Lean, trying to prove the next lemma: lemma l1_cl (A B C : Prop) : ((A → B) → C) → ((A ∧ ¬ B) ∨ C) := …
|
|
Assuming I have some definition with a forall and an exists like so: Definition fooable A B P := forall a : A, exists b : B, P a b. Then on an intuitive level, I …
|
|
The docs on lambdas in Agda provide two forms of lambda: a curly brace based version, and the where syntax. But while writing some programs, I stumbled across a third version: one pattern, no braces, …
|
|
When I first learned Haskell, I was told that you use data keyword to define an “algebraic data type”, or a “sum type”. Then I learned the idea …
|
|
I’m working in cubical agda. I am wondering how to access local definitions once outside of the local environment. For example, suppose I have the following code: …
|
