7 lines
78 B
Agda
7 lines
78 B
Agda
module LowerPatVar
|
||
|
||
import Prelude
|
||
|
||
foo : Nat × Nat → Nat
|
||
foo (ZZ , y) = Z
|