Questions tagged [rewriting]

In a rewriting system, one specifies a set of rules that describe valid replacements of subformulae by other ones. (from nLab).

2 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
2 votes
1 answer

Debug autorewrite in Coq

I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting) I then manually figure out which rewrite rules were ...
8bc3 457f's user avatar
  • 224
1 vote
0 answers

Can you help me lay out the different variations of CoC and their generalizations?

I am learning the typed lambda-calculus and looking into the Calculus of Constructions. It was going well until I was slapped in the face with variations, and now I'm confused about the layout of all ...
Alex Byard's user avatar