Create Data.Reify
This commit is contained in:
parent
cc1cef621b
commit
e694536939
13
src/Data/Reify.idr
Normal file
13
src/Data/Reify.idr
Normal file
|
@ -0,0 +1,13 @@
|
||||||
|
module Data.Reify
|
||||||
|
|
||||||
|
%default total
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
data Reify : a -> Type where
|
||||||
|
MkReify : (x : a) -> Reify x
|
||||||
|
|
||||||
|
public export
|
||||||
|
getReify : {0 x : a} -> Reify x -> a
|
||||||
|
getReify (MkReify x) = x
|
||||||
|
|
Loading…
Reference in a new issue