All Questions
50
questions
-4
votes
1
answer
335
views
Can a dependently typed language be Turing complete? [closed]
It seems as though dependently typed languages are often not Turing complete. Why can we not allow every function to have general recursion (which would make the language Turing complete), instead of ...
0
votes
2
answers
87
views
Is there a function that returns a list of values with specific type in OCaml?
In Haskell, using listify with Data can extract values of a specific type from a deeply nested structure without lots of getters. For example, with the following code:
{-# LANGUAGE DeriveDataTypeable #...
- 874
0
votes
1
answer
78
views
How to extract the exact information of `GenArg`?
I'm writing a Coq formatter (code). So far, I got the AST of a Coq code and pretty-printed a few of its nodes. However, I cannot pretty-print VernacExtend nodes.
The CoqAst below represents the AST of ...
- 874
1
vote
2
answers
251
views
How to generate the AST of a Coq source code?
I'm trying to write a Coq source code formatter, and I want the AST for a Coq source code.
Firstly I tried to generate ASTs from the official Coq library but gave it up because I couldn't know how.
...
- 874
0
votes
3
answers
307
views
How does one pin/freeze a version of the dependencies of an opam project/package and then install the project with such specified dependencies?
How do we freeze an entire dependency tree/chain from an already working opam install?
I have a bunch of coq projects installed via opam right now. I'd like to figure out what commit they are using ...
- 5,961
1
vote
1
answer
240
views
How do I install ocamlfind first properly before other opam packages without root permissions?
I was trying to install some coq packages with opam but have this hack:
# coq-equations seems to rely on ocamlfind for it's build, but doesn't
# list it as a dependency, so opam sometimes tries to ...
- 5,961
0
votes
1
answer
105
views
How to install the coq 8.14 (or 8.15) package with opam pin when it says it can't find it?
I am on ubuntu. I'm trying to install coq 8.14. I'm sure it must exist. Why doesn't it let me install it? Commands and error msg:
(iit_synthesis) brando9~/proverbot9001 $ opam switch create coq-8.14 4....
- 5,961
0
votes
1
answer
109
views
Printing Coq definition without loading library
Coq is using a module system similar to OCaml. In OCaml, we can apply a function like Module_A.Module_B.Func and use Module_A.Module_B. to find the path to Func.
However, I cannot do similar things in ...
- 25
2
votes
1
answer
406
views
Adding an old version of Ocaml to Opam
I am trying to install Coq version 8.10.2 using Opam and from this output, I assume Coq 8.10.2 needs an ocaml compiler with version < 4.10
Missing dependency:
- (invariant) -> coq = 8.10.2 -&...
2
votes
1
answer
549
views
Problem with Ocaml and make: "Error: the file ____.cmxa is not a compilation unit description"
I'm running make in the top level of the UniMath directory and make keeps returning errors. I'm working on fedora 35 and I'm using Ocaml version 4.11.2.
Here is a print out of the errors
make[2]: ...
- 207
0
votes
2
answers
252
views
Proving an addition function is associative using Coq
I am trying to prove that a predefined addition function is associative, but I am stuck at the step where the goal reads
plus (S x') (plus y z) = plus (plus (S x') y) z
but the only hypothesis I have ...
- 1
2
votes
1
answer
130
views
How to get the name of a named goal in the coq api
I'm currently working on an ocaml program, which will be using the coq api to extract information about proofs and their goals.
For this, I want to extract the name given to a goal, when a "...
- 21
0
votes
0
answers
279
views
Installing library for Coq via Opam on Windows
I'm know nothing in programming. During the installation via Opam library Math Classes in Coq i received an ERROR. I don't know what to do, no idea. The same ERROR occurs when i try to install Bignums ...
- 1
2
votes
1
answer
267
views
coq 8.11.0 incompatible with ocaml 4.10?
I am installing coq with opam as per these instructions and have gotten the error message
`No solution for coq: The following dependencies couldn't be met:
- coq → ocaml < 4.10
...
- 437
2
votes
1
answer
100
views
Inspecting elements of an inductive type from OCaml
I would like to write a Coq plugin which would take an element of an inductive type and recursively pattern match on the element and preform some computation in each iteration. This sounds like a ...
- 1,590