Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Cube/Cube.thy
changeset 24783 5a3e336a2e37
parent 22809 3cf5df73d50a
child 26956 1309a6a0a29f
equal deleted inserted replaced
24782:38e5c05ef741 24783:5a3e336a2e37 
    12 typedecl "term"
 
    12 typedecl "term"
 
    13 typedecl "context"
 
    13 typedecl "context"
 
    14 typedecl typing
 
    14 typedecl typing
 
    15 
    15 
    16 nonterminals
 
    16 nonterminals
 
    17   context_ typing_
 
    17   context' typing'
 
    18 
    18 
    19 consts
 
    19 consts
 
    20   Abs           :: "[term, term => term] => term"
 
    20   Abs           :: "[term, term => term] => term"
 
    21   Prod          :: "[term, term => term] => term"
 
    21   Prod          :: "[term, term => term] => term"
 
    22   Trueprop      :: "[context, typing] => prop"
 
    22   Trueprop      :: "[context, typing] => prop"
 
    26   box           :: "term"                               ("[]")
 
    26   box           :: "term"                               ("[]")
 
    27   app           :: "[term, term] => term"               (infixl "^" 20)
 
    27   app           :: "[term, term] => term"               (infixl "^" 20)
 
    28   Has_type      :: "[term, term] => typing"
 
    28   Has_type      :: "[term, term] => typing"
 
    29 
    29 
    30 syntax
 
    30 syntax
 
    31   Trueprop      :: "[context_, typing_] => prop"        ("(_/ |- _)")
 
    31   Trueprop      :: "[context', typing'] => prop"        ("(_/ |- _)")
 
    32   Trueprop1     :: "typing_ => prop"                    ("(_)")
 
    32   Trueprop1     :: "typing' => prop"                    ("(_)")
 
    33   ""            :: "id => context_"                     ("_")
 
    33   ""            :: "id => context'"                     ("_")
 
    34   ""            :: "var => context_"                    ("_")
 
    34   ""            :: "var => context'"                    ("_")
 
    35   MT_context    :: "context_"                           ("")
 
    35   MT_context    :: "context'"                           ("")
 
    36   Context       :: "[typing_, context_] => context_"    ("_ _")
 
    36   Context       :: "[typing', context'] => context'"    ("_ _")
 
    37   Has_type      :: "[term, term] => typing_"            ("(_:/ _)" [0, 0] 5)
 
    37   Has_type      :: "[term, term] => typing'"            ("(_:/ _)" [0, 0] 5)
 
    38   Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
 
    38   Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
 
    39   Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
 
    39   Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
 
    40   arrow         :: "[term, term] => term"               (infixr "->" 10)
 
    40   arrow         :: "[term, term] => term"               (infixr "->" 10)
 
    41 
    41 
    42 translations
 
    42 translations
 
    44   "Lam x:A. B"   == "Abs(A, %x. B)"
 
    44   "Lam x:A. B"   == "Abs(A, %x. B)"
 
    45   "Pi x:A. B"    => "Prod(A, %x. B)"
 
    45   "Pi x:A. B"    => "Prod(A, %x. B)"
 
    46   "A -> B"       => "Prod(A, %_. B)"
 
    46   "A -> B"       => "Prod(A, %_. B)"
 
    47 
    47 
    48 syntax (xsymbols)
 
    48 syntax (xsymbols)
 
    49   Trueprop      :: "[context_, typing_] => prop"        ("(_/ \<turnstile> _)")
 
    49   Trueprop      :: "[context', typing'] => prop"        ("(_/ \<turnstile> _)")
 
    50   box           :: "term"                               ("\<box>")
 
    50   box           :: "term"                               ("\<box>")
 
    51   Lam           :: "[idt, term, term] => term"          ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
 
    51   Lam           :: "[idt, term, term] => term"          ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
 
    52   Pi            :: "[idt, term, term] => term"          ("(3\<Pi> _:_./ _)" [0, 0] 10)
 
    52   Pi            :: "[idt, term, term] => term"          ("(3\<Pi> _:_./ _)" [0, 0] 10)
 
    53   arrow         :: "[term, term] => term"               (infixr "\<rightarrow>" 10)
 
    53   arrow         :: "[term, term] => term"               (infixr "\<rightarrow>" 10)
 
    54 
    54
isabelle