Questions tagged [definition]

The tag has no usage guidance.

2 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
5 votes
0 answers
217 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 ...
user695931's user avatar
2 votes
1 answer
134 views

Is there a way to rename parameters when including/reusing a module type in Coq?

Say I have a (more general) module type Collection that specifies some operations like read and write and now I want to create (more specialized) module types like <...
C.E.Sally's user avatar
  • 121