8 lines
56 B
Agda
8 lines
56 B
Agda
module TestImport
|
|
|
|
import Prelude
|
|
|
|
one : Nat
|
|
one = S Z
|
|
|