Proving metatheorems talk:Representing the judgements of the natural numbers
From The Twelf Project
Shouldn't "i.e., it is the specialization of the inference rule to 
" read "i.e., it is the specialization of the inference rule to 
", since only a small n appears in the judgements?
- Fixed. Thanks again! If you like, feel free to fix typos like this directly in the text. Drl 11:30, 18 April 2007 (EDT)
[edit] %worlds
The %worlds page said
As discussed in the introduction article on Representing the judgments of the natural numbers, the type nat in this signature adequately represents the natural numbers only if the LF context does not contain variables of type nat.
This page doesn't mention that now, but I would be very grateful if it did!
- Fixed--thanks! Drl 17:16, 25 July 2008 (EDT)
