rule ℕ type;;
rule B type;;
rule a : ℕ;;
rule b : ℕ;;
?? type;;
{x : ℕ} {y : ℕ} (⁇ type) ;;
⁇ : ℕ ;;
{x : ℕ} {y : ℕ} ⁇ : ℕ ;;
ℕ ≡ B as ?? ;;
{x : ℕ} {y : ℕ} ℕ ≡ B as ?? ;;
a ≡ b : ℕ as ?? ;;
{x : ℕ} a ≡ x : ℕ as ?? ;;
(*Checking judgements against boundaries*)
ℕ :? (?? type);;
a :? (?? : ℕ);;
(*Match on boundaries and judgements*)
let c = {n : ℕ} n;;
let m = match c with {y : Y} w :> judgement -> (y,Y,w) end;;
let d = {n : ℕ} ?? : ℕ;;
let k = match d with {_ : _} w :> boundary -> w end;;