Input

Language Grammar
  • !/⊥: The bottom type
  • */⊤: The top type
  • A&B/A∧B: An intersection type
  • A|B/A∨B: A union type
  • A->B/A→B: An arrow (function) type
  • A??B: A judgement query for the relationship between A and B, which will be answered in the output editor.
  • Other types: Identifiers beginning with an uppercase letter are treated as primitive types.j Full Parser Specification
Source

Judgements

398bb2c