As of May 31, 2023, we have updated our Code of Conduct.

Questions tagged [definition]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
5 votes
2 answers

Unclarity about Preorder class in Lean4

I realize the port of Mathlib to Lean4 is not finished yet, but I've run into a definition that I do not quite understand. I'm quite new at using theoremprovers as well as stackexchange, so please be ...
Pieter Cuijpers's user avatar
5 votes
0 answers

An algorithm for the substitution of formulas for predicates in first order logic

I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is ...
user695931's user avatar
3 votes
2 answers

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

I'm trying to formalize a small part of higher-order arithmetic in Coq as an exercise (Wikipedia article for second-order arithmetic). It's straightforward to formalize something resembling second-...
Greg Nisbet's user avatar
  • 2,671
2 votes
1 answer

How do clausal definitions work?

I'm most familiar with the metatheory of calculi based around expressions. But systems like Agda use separate clauses for definitions. ...
Molly Stewart-Gallus's user avatar
1 vote
1 answer

Question about default definitions in fields

In Unclarity about Preorder class in Lean4 I asked why the third and fourth field (lt and lt_iff_le_not_le) in the definition of MyPreorder below would both be necessary, as one follows from the other ...
Pieter Cuijpers's user avatar
0 votes
1 answer

Define a function using another function

I want to define a translation function g from another function f. Definition trans (f g : Q -> Q) (t : Q) := forall q : Q, f (q + t) == g q. In the above code,...
with-forest's user avatar