first-order/syntax/modules.elf

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "base.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Forall = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder  %include BaseFOL   %open o i.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder  forall : (i -> o) -> o.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Exists = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder  %include BaseFOL   %open o i.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder  exists : (i -> o) -> o.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Equal = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder  %include BaseFOL   %open o i.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder  eq : i -> i -> o.  %infix none 25 eq.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova}.