| The Coq Proof Assistant - Reference Manual V 5.10 (1995) | |||||||||||||||
Abstract | |||||||||||||||
| ion All Axiom Begin Cd Chapter Check CheckGuard CoFixpoint Compute Defined Definition Drop Elimination End Eval Explain Extraction Fact Fixpoint Focus for Go Goal Hint Hypothesis Immediate Induction Inductive Infix Inspect Lemma Let Local Minimality ML Module Modules Mutual Node Opaque Parameter Parameters Print Proofs Prop Pwd Qed Remark Require Restart Resume Save Scheme Script Search Section Set Show Silent States Suspend Syntactic Theorem Token Transparent Tree Type TypeSet Undo Unfocus Variable Variables Write Other keywords and user's tokens The following sequences of characters are also keywords: --- : := = ? ?? !? !! ! -? ; # * , ? @ :: / !- You can add new tokens with the command Token (see section 5.7.4). New tokens must be sequences, without blanks, of characters taken from the following list: ! ? / " - + = ; , --- ! @ # % & ? * : ~ $ a..z A..Z ' 0..9 that do not start with a character from $ a..z A..Z ' 0..9 Lexical ambiguities are resolved according to the "longest m... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||