{
  "terms": {
    "name": "judge_t",
    "types": [
      {
        "type_name": "var_t",
        "constrs": [
          {
            "constr_name": "v",
            "args": [ { "arg_name": "x1", "arg_type": [ "StringT" ] } ],
            "draw": [ [ "Arg", "x1" ] ]
          }
        ]
      },
      {
        "type_name": "value_t",
        "constrs": [
          {
            "constr_name": "var",
            "args": [ { "arg_name": "x1", "arg_type": [ "RecT", "var_t" ] } ],
            "draw": [ [ "Arg", "x1" ] ]
          },
          {
            "constr_name": "fun",
            "args": [
              { "arg_name": "x1", "arg_type": [ "RecT", "var_t" ] },
              { "arg_name": "e2", "arg_type": [ "RecT", "term_t" ] }
            ],
            "draw": [
              [ "Str", "fun " ],
              [ "Arg", "x1" ],
              [ "Str", "-> " ],
              [ "Arg", "e2" ]
            ]
          }
        ]
      },
      {
        "type_name": "term_t",
        "constrs": [
          {
            "constr_name": "val",
            "args": [
              { "arg_name": "v1", "arg_type": [ "RecT", "value_t" ] }
            ],
            "draw": [ [ "Arg", "v1" ] ]
          },
          {
            "constr_name": "app",
            "args": [
              { "arg_name": "e1", "arg_type": [ "RecT", "term_t" ] },
              { "arg_name": "e2", "arg_type": [ "RecT", "term_t" ] }
            ],
            "draw": [ [ "Arg", "e1" ], [ "Str", " @ " ], [ "Arg", "e2" ] ]
          }
        ]
      },
      {
        "type_name": "tvar_t",
        "constrs": [
          {
            "constr_name": "tv",
            "args": [ { "arg_name": "t1", "arg_type": [ "StringT" ] } ],
            "draw": [ [ "Arg", "t1" ] ]
          }
        ]
      },
      {
        "type_name": "type_t",
        "constrs": [
          { "constr_name": "int", "args": [], "draw": [ [ "Str", "int" ] ] },
          {
            "constr_name": "tvar",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "tvar_t" ] }
            ],
            "draw": [ [ "Arg", "t1" ] ]
          },
          {
            "constr_name": "arrow",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "type_t" ] }
            ],
            "draw": [ [ "Arg", "t1" ], [ "Str", " => " ], [ "Arg", "t1" ] ]
          }
        ]
      },
      {
        "type_name": "env_t",
        "constrs": [
          { "constr_name": "empty", "args": [], "draw": [ [ "Str", "[]" ] ] },
          {
            "constr_name": "cons",
            "args": [
              { "arg_name": "x1", "arg_type": [ "RecT", "var_t" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "e3", "arg_type": [ "RecT", "env_t" ] }
            ],
            "draw": [
              [ "Str", "( " ],
              [ "Arg", "x1" ],
              [ "Str", " , " ],
              [ "Arg", "t2" ],
              [ "Str", " ) :: " ],
              [ "Arg", "e3" ]
            ]
          }
        ]
      },
      {
        "type_name": "judge_t",
        "constrs": [
          {
            "constr_name": "judge",
            "args": [
              { "arg_name": "env", "arg_type": [ "RecT", "env_t" ] },
              { "arg_name": "term", "arg_type": [ "RecT", "term_t" ] },
              { "arg_name": "type", "arg_type": [ "RecT", "type_t" ] }
            ],
            "draw": [
              [ "Arg", "env" ],
              [ "Str", " |- " ],
              [ "Arg", "term" ],
              [ "Str", " : " ],
              [ "Arg", "type" ]
            ]
          },
          {
            "constr_name": "equal",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "type_t" ] }
            ],
            "draw": [ [ "Arg", "t1" ], [ "Str", " = " ], [ "Arg", "t2" ] ]
          }
        ]
      }
    ]
  },
  "infers": [
    {
      "name": "tapp",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [ "M", "env_t", "env" ],
              [
                "V",
                "term_t",
                "app",
                [ [ "M", "term_t", "tm1" ], [ "M", "term_t", "tm2" ] ]
              ],
              [ "M", "type_t", "tp2" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "judge",
              [
                [ "M", "env_t", "env" ],
                [ "M", "term_t", "tm1" ],
                [
                  "V",
                  "type_t",
                  "arrow",
                  [ [ "M", "type_t", "tp1" ], [ "M", "type_t", "tp2" ] ]
                ]
              ]
            ],
            [
              "V",
              "judge_t",
              "judge",
              [
                [ "M", "env_t", "env" ],
                [ "M", "term_t", "tm2" ],
                [ "M", "type_t", "tp1" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "tfun",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [ "M", "env_t", "env" ],
              [
                "V",
                "term_t",
                "val",
                [
                  [
                    "V",
                    "value_t",
                    "fun",
                    [ [ "M", "var_t", "x" ], [ "M", "term_t", "tm" ] ]
                  ]
                ]
              ],
              [
                "V",
                "type_t",
                "arrow",
                [ [ "M", "type_t", "tp1" ], [ "M", "type_t", "tp2" ] ]
              ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "judge",
              [
                [
                  "V",
                  "env_t",
                  "cons",
                  [
                    [ "M", "var_t", "x" ],
                    [ "M", "type_t", "tp1" ],
                    [ "M", "env_t", "env" ]
                  ]
                ],
                [ "M", "term_t", "tm" ],
                [ "M", "type_t", "tp2" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "tvarzero",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [
                "V",
                "env_t",
                "cons",
                [
                  [ "M", "var_t", "x" ],
                  [ "M", "type_t", "tp1" ],
                  [ "M", "env_t", "env" ]
                ]
              ],
              [
                "V",
                "term_t",
                "val",
                [ [ "V", "value_t", "var", [ [ "M", "var_t", "x" ] ] ] ]
              ],
              [ "M", "type_t", "tp2" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "equal",
              [ [ "M", "type_t", "tp1" ], [ "M", "type_t", "tp2" ] ]
            ]
          ]
        }
      ]
    },
    {
      "name": "tvarsuc",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [
                "V",
                "env_t",
                "cons",
                [
                  [ "M", "var_t", "y" ],
                  [ "M", "type_t", "tp1" ],
                  [ "M", "env_t", "env" ]
                ]
              ],
              [
                "V",
                "term_t",
                "val",
                [ [ "V", "value_t", "var", [ [ "M", "var_t", "x" ] ] ] ]
              ],
              [ "M", "type_t", "tp2" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "judge",
              [
                [ "M", "env_t", "env" ],
                [
                  "V",
                  "term_t",
                  "val",
                  [ [ "V", "value_t", "var", [ [ "M", "var_t", "x" ] ] ] ]
                ],
                [ "M", "type_t", "tp2" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "tequal",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "judge_t",
            "equal",
            [ [ "M", "type_t", "tp" ], [ "M", "type_t", "tp" ] ]
          ]
        }
      ]
    }
  ],
  "input" :  [ "M", "judge_t", "j" ]
}