mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-29 03:24:02 +03:00
31 lines
575 B
Idris
31 lines
575 B
Idris
import Data.Vect
|
|
|
|
MkBig : Nat -> Type
|
|
MkBig Z = Int
|
|
MkBig (S k) = ((n ** Vect n Int), MkBig k)
|
|
|
|
bigEx : (n : Nat) -> MkBig n
|
|
bigEx Z = 94
|
|
bigEx (S k) = ((2 ** [0,0]), bigEx k)
|
|
|
|
data VWrap : Type -> Type where
|
|
MkVWrap : (0 n : Nat) -> Vect n a -> VWrap a
|
|
|
|
export
|
|
MkBig' : Nat -> Type
|
|
MkBig' Z = Int
|
|
MkBig' (S k) = (VWrap Int, MkBig' k)
|
|
|
|
namespace Foo
|
|
public
|
|
export
|
|
bigEx' : (n : Nat) -> MkBig' n
|
|
bigEx' Z = 94
|
|
bigEx' (S k) = (MkVWrap 1 [0], bigEx' k)
|
|
|
|
eqBigs : bigEx 1000000 = bigEx 1000000
|
|
eqBigs = Refl
|
|
|
|
eqBigs' : bigEx' 800000 = bigEx' 800000
|
|
eqBigs' = Refl
|