Commit 27818ed2 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Notation for type variables.

parent 54067433
......@@ -14,6 +14,7 @@ Inductive ty :=
Delimit Scope ty_scope with ty.
Bind Scope ty_scope with ty.
Notation "# x" := (TVar x) : ty_scope.
Notation "()" := TUnit : ty_scope.
Infix "*" := TProd : ty_scope.
Infix "+" := TSum : ty_scope.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment