Top new questions this week:
|
|
Many proof assistants have a way to make certain arguments of a function as “implicit”, so that the user doesn’t have to supply them but they will be solved by unification. Sometimes, such …
|
|
I am new to lean, working on proving a simple lemma in lean4. lemma String.split_empty (c): String.split “” c = [“”] I tried looking for …
|
|
I heard that untyped lambda expressions can have no normal forms. As an example, the expression $(\lambda x. x\space x) (\lambda x. x\space x)$ , when put to a $\beta$ conversion, gives back the same …
|
|
Suppose I have a unification problem a b = f u Where f is neutral and u is WHNF and …
|
|
I’m trying out Agda’s Foreign Function Interface with a simple correctness proof of quicksort (which I have defined in Haskell), but I’m having trouble importing the Haskell function. I’ve been …
|
Greatest hits from previous weeks:
|
|
Ever since the work by Gimenez for his PhD thesis, Coq has supported positive coinductive types. For example, the type of always-infinite streams containing elements of type …
|
|
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: …
|
|
As far as I know, the default configuration for the Lean VSCode plugin checks the code continuously, and so even when the user is in the middle of typing an expression, Lean will immediately report a …
|
|
Higher structures in category theory lead very organically to visual or graphical interpretations in terms of string diagrams and commuting squares. However, it seems hard to implement a graphical …
|
|
I find my mathematics and programming background$^*$ do not endow me with much understanding of type theory as it pertains to proof assistants. To remedy this shortcoming I don’t expect a Royal Road …
|
|
The Natural Number Game suggests the possibility of rewriting mathematics textbooks with embedded interactive Lean code. I’m envisioning something like Google Colab or Mathematica, where you can …
|
|
Is there a library (for any proof assistant) which provides formalized definitions of unsolved problems? To clarify, I mean some collection that correctly defines unsolved problems in the language of …
|
