[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Hourly clock spec: why it needs the temporal-logic operator box 
You say that HCnxt is, by definition, always true. By that reasoning, if the spec had defined HCini to equal hr = 1, would that always be true? How would you specify an hour clock that had to begin with hr = 1? And if I were to write the definition
FalseTheorem == 1+2 = 4
would that mean that 1+2 = 4 is always true? What is the difference between a definition and a theorem?