18 lines
288 B
Agda
18 lines
288 B
Agda
data Greeting : Set where
|
||
hello : Greeting
|
||
|
||
greet : Greeting
|
||
greet = hello
|
||
|
||
module hello-world-dep where
|
||
|
||
open import Data.Nat using (ℕ; zero; suc)
|
||
|
||
data Vec (A : Set) : ℕ → Set where
|
||
[] : Vec A zero
|
||
_∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
|
||
|
||
infixr 5 _∷_
|
||
|
||
|