Duck Language Syntax
<Duck_Script> ::= ( <Global_Declaration> | <Proof_Declaration> | <Display_Declaration> )+ <Global_Declaration> :: = <Project_Declaration> | <Markup_Declaration> | <Style_Declaration> | <Spec_Declaration> | <Dir_Declaration> | <Induction_Scheme_Declaration> | <Relation_Declaration> | <Cobasis_Declaration> <Project_Declaration> ::= project: <Identifier> (. <Identifier> )* <Markup_Declaration> :: = markup: <Identifier> <Style_Declaration> ::= style: <Identifier> <Spec_Declaration> ::= spec: <File_Path_Name> <Dir_Declaration> ::= dir: <File_Path_Name> <Induction_Scheme_Declaration> ::= induction-scheme: <Identifier> sort <Sort_Name> . assertion <Op_Name> : (<Sort_Name>)+ . (<Base_Case_Declaration> | <Induction_Case_Declaration>)+ [] <Base_Case_Declaration> ::= base <Formula> . <Induction_Case_Declaration> ::= induction ops <Identifier> : -> <Sort_Name> . assume (<Formula>)+ . goal <Formula> . <Relation_Declaration> ::= relation: (<BOBJ_Variable> | <BOBJ_Operator> | <BOBJ_Equation>)+ [] <Cobasis_Declaration> ::= cobasis: (<BOBJ_Operator>)+ [] <Proof_Declaration> ::= <Proof_Header> (<Proof_Rule>)+ [] <Proof_Header> ::= << <Identifier> >> [ <Spec_Declaration> ] <Goal_Declaration> <Goal_Declaration> ::= assoc-of <BOBJ_Operator_Name> | comm-of <BOBJ_Operator_Name> | <Formula> <Proof_Rule> ::= auto | show | mk-conj (<Identifier>)+ [ >> { <Identifier> } ] | case-anal <Identifier> [ >> { (<Identifier>)+ } ] | exq-let <Identifier> = <BOBJ_Term> ( ; <Identifier> = <BOBJ_Term> )* | op-apply <BOBJ_Operation_Name> (<Identifier>)+ [ >> { <Identifier> } ] | to-rule <Identifier> | de-conj [ <Identifier> ] [ >> { (<Identifier>)+ } ] | skolem [ <Identifier> ] [ >> { <Identifier> } ] | modus <Identifier> <Identifier> [ >> { <Identifier> } ] | backward [ <Identifier> ] [ >> { <Identifier> } ] | eq-apply <Identifier> <Identifier> [ >> { <Identifier> } ] | instance [ <Identifier> ] with <BOBJ_Term> [ >> { <Identifier> } ] | neg-elim | ( coind | coinduction | ex-coind) | imp-elim [ >> { <Identifier> } ] | conj-elim | uq-elim | all-uq-elim | assume <Formula> | lemma <Identifier> [ >> { <Identifier> } ] | induction on <BOBJ_Variable_Name> [ : <BOBJ_Sort> ] [ ( by | with ) scheme ( <BOBJ_Operation_List> | <Identifier> ) ] | red [ <Identifier> ] | test-red <Formula> ::= ( <Formula> ) | <BOBJ_Equation> | not <Formula> | <Formula> and <Formula> | <Formula> or <Formula> | <Formula> implies <Formula> | ( forall | exists ) ((<Identifier>)+ : <BOBJ_Sort>)+ <Formula> <Display_Declaration> ::= display: << (<Identifier>)+ >> <Display_Header> (<Page_Declaration>)+ [] <Display_Header> ::= ( homepage: <File_Path_Name> | title: <String_Literal> | dir: <File_Path_Name> | specexpl: <File_Path_Name> | closing: <File_Path_Name> )* <Page_Declaration> ::= << <Identifier> (. <Identifier>)* >> intro: <String_Literal> subtitle: <String_Literal> expl: <File_Path_Name> ( [;] <Page_Declaration> )*
To the Tatami project homepage
To the Kumo homepage
To the Duck homepage
Maintained by Joseph Goguen
Last modified 11 October 2001