python (65.2k questions)

javascript (44.3k questions)

reactjs (22.7k questions)

java (20.8k questions)

c# (17.4k questions)

html (16.3k questions)

r (13.7k questions)

android (13k questions)

Questions - proof-assistant

How does one build the list of only true elements in Coq using dependent types?

I was going through the Coq book from the maths perspective. I was trying to define a dependently typed function that returned a length list with n trues depending on the number trues we want. Coq com...
test-img

Charlie Parker

coq

dependent-type

proof-assistant

Votes: 0

Answers: 1

Latest Answer

In this case, it looks like Coq does not manage to infer the return type of the match expression, so the best thing to do is to give it explicitly: Fixpoint g (n : nat) : t n := match n return t n w...
test-img

Théo Winterhalter

How does one define dependent type with named arguments in Coq without issues in unification in the constructors?

I want to defined a lenghted list but I like arguments with names at the top of the inductive definition. Whenever I try that I get unification errors with things I hoped worked and was forced to do a...
test-img

Charlie Parker

coq

dependent-type

theorem-proving

proof-assistant

Votes: 0

Answers: 1

Latest Answer

Named arguments to the left of : (they are called parameters) are implicitly forall'd in each constructor and must appear as the same variable in the return type of each constructor. Arguments to the ...
test-img

HTNW

Posts

Questions

Blogs

Jobs