7 votes
Accepted

Coq defining a hierarchy of collections of integers with infinitely many "levels"

A simple way is to define the type in terms of the Peano natural numbers nat. ...
Bubbler's user avatar
  • 674
5 votes
Accepted

Unclarity about Preorder class in Lean4

The extra fields are a convenience. It is useful to have both $<$ and $\leq$ at disposal when working with preorders, so how can we have that? We could decide which one is “primary”, include it in ...
Andrej Bauer's user avatar
  • 8,969
3 votes

Unclarity about Preorder class in Lean4

[Edit: I completely rewrote this answer.] I would say that Andrej's answer is only half the story. Lean uses type classes for overloading notation. If I have ...
Jason Rute's user avatar
  • 8,495
3 votes
Accepted

Define a function using another function

Do you mean a functional like below ? ...
Pierre Castéran's user avatar
3 votes
Accepted

How do clausal definitions work?

If you are interested in non-dependent languages then it is probably not a proof-assistants related question. Those are quite well-studied in computer science. So I assume you are asking about using ...
Trebor's user avatar
  • 3,867
2 votes

Defining a Recursive Function decreasing on one argument with < and another structurally

I rephrased the * case into : ...
Pierre Castéran's user avatar
1 vote

Question about default definitions in fields

Thanks to Jason Rute his comment, I think I can now answer my own question partially. I figured out that my example does not typecheck in isolation, whereas it did in my sandbox file because there was ...
Pieter Cuijpers's user avatar
1 vote

Coq defining a hierarchy of collections of integers with infinitely many "levels"

Your definition is awkward because of strict positivity requirements in inductive datatypes. Your definition of col is really a decidable subset and there exists an ...
Molly Stewart-Gallus's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible