Skip to content

Instantly share code, notes, and snippets.

@georgelesica-wf

georgelesica-wf/Landscape.idr

Created September 15, 2015 00:28
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save georgelesica-wf/0c15c48e6a3334c531fe to your computer and use it in GitHub Desktop.
Save georgelesica-wf/0c15c48e6a3334c531fe to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Landscape.idr
module Landscape
data Landscape : Nat -> Nat -> Double -> Type where
NK : (n : Nat) -> (k : Nat) -> Landscape n k 0.0
NKp : (n : Nat) -> (k : Nat) -> (p : Float) -> Landscape n k p
getN : Landscape n _ _ -> Nat
getN _ = n
getK : Landscape _ k _ -> Nat
getK _ = k
getP : Landscape _ _ p -> Double
getP _ = p
-- record Model (n : Nat) (k : Nat) where
-- constructor MkLandscape
-- landscape : N
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment