Duck Language Syntax
::=
( | | )+
:: =
|
|
|
|
|
|
|
::= project: (. )*
:: = markup:
::= style:
::= spec:
::= dir:
::=
induction-scheme:
sort .
assertion : ()+ .
( | )+
[]
::= base .
::=
induction
ops : -> .
assume ()+ .
goal .
::=
relation: ( | | )+ []
::= cobasis: ()+ []
::= ()+ []
::=
<< >> [ ]
::=
assoc-of
| comm-of
|
::=
auto
| show
| mk-conj ()+ [ >> { } ]
| case-anal [ >> { ()+ } ]
| exq-let
=
( ; = )*
| op-apply
()+
[ >> { } ]
| to-rule
| de-conj [ ] [ >> { ()+ } ]
| skolem [ ] [ >> { } ]
| modus [ >> { } ]
| backward [ ] [ >> { } ]
| eq-apply [ >> { } ]
| instance [ ] with
[ >> { } ]
| neg-elim
| ( coind | coinduction | ex-coind)
| imp-elim [ >> { } ]
| conj-elim
| uq-elim
| all-uq-elim
| assume
| lemma [ >> { } ]
| induction on [ : ]
[ ( by | with ) scheme
( | ) ]
| red [ ]
| test-red
::=
( )
|
| not
| and
| or
| implies
| ( forall | exists ) (()+ : )+
::=
display: << ()+ >>
()+
[]
::=
( homepage:
| title:
| dir:
| specexpl:
| closing: )*
::=
<< (. )* >>
intro:
subtitle:
expl:
( [;] )*
To the Tatami project homepage
To the Kumo homepage
To the Duck homepage
Maintained by Joseph Goguen
Last modified 11 October 2001