Questions tagged [definition]
The definition tag has no usage guidance.
6
questions
5
votes
2
answers
157
views
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 ...
- 133
5
votes
0
answers
198
views
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 ...
- 409
3
votes
2
answers
179
views
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-...
- 2,671
2
votes
1
answer
72
views
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.
...
- 2,678
1
vote
1
answer
57
views
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 ...
- 133
0
votes
1
answer
64
views
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,...
- 337