Questions tagged [definition]
The definition tag has no usage guidance.
7
questions
1
vote
2
answers
73
views
Defining a Recursive Function decreasing on one argument with < and another structurally
I want to define a function which decreases in one argument using < and on another structurally. What is the least painful way to do this? Among the many options (Function, Program Fixpoint, ...
- 1,241
2
votes
1
answer
73
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,768
1
vote
1
answer
58
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 ...
- 143
5
votes
2
answers
211
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 ...
- 143
0
votes
1
answer
72
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,...
- 357
5
votes
0
answers
205
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 ...
- 419
4
votes
2
answers
191
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,711