Don't allow uppercase pattern variables

This commit is contained in:
2026-02-20 16:12:54 -08:00
parent 7d5789147d
commit c54b856f0b
5 changed files with 24 additions and 2 deletions

6
tests/LowerPatVar.newt Normal file
View File

@@ -0,0 +1,6 @@
module LowerPatVar
import Prelude
foo : Nat × Nat Nat
foo (ZZ , y) = Z

View File

@@ -0,0 +1,10 @@
*** Process tests/LowerPatVar.newt
module Prelude
module LowerPatVar
ERROR at tests/LowerPatVar.newt:6:6--6:8: ZZ not in scope
foo : Nat × Nat → Nat
foo (ZZ , y) = Z
^^
ERROR at tests/LowerPatVar.newt:1:1--1:1: Compile failed

View File

@@ -66,7 +66,7 @@ data Sg : (A : U) -> (A -> U) -> U where
_,_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B
_*_ : U -> U -> U
A * B = Sg A (\ _ => B)
a * b = Sg a (\ _ => b)
TooBig : Bnd -> Bnd -> Nat -> U
TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h)