31 lines
599 B
Idris
31 lines
599 B
Idris
|
module Quox.Eval
|
||
|
|
|
||
|
|
-- todo list:
|
||
|
|
-- - understand nbe and use it
|
||
|
|
-- - take a proof of well-typedness as an argument
|
||
|
|
|
||
|
|
import Quox.Syntax
|
||
|
|
|
||
|
|
import Data.DPair
|
||
|
|
|
||
|
|
%default total
|
||
|
|
|
||
|
|
|
||
|
|
public export Exists2 : (ty1 -> ty2 -> Type) -> Type
|
||
|
|
Exists2 t = Exists (\a => Exists (\b => t a b))
|
||
|
|
|
||
|
|
public export SomeTerm : Type
|
||
|
|
SomeTerm = Exists2 Term
|
||
|
|
|
||
|
|
public export SomeElim : Type
|
||
|
|
SomeElim = Exists2 Elim
|
||
|
|
|
||
|
|
public export SomeDim : Type
|
||
|
|
SomeDim = Exists Dim
|
||
|
|
|
||
|
|
private some : {0 t : ty -> Type} -> t a -> Exists t
|
||
|
|
some t = Evidence ? t
|
||
|
|
|
||
|
|
private some2 : {0 t : ty1 -> ty2 -> Type} -> t a b -> Exists2 t
|
||
|
|
some2 t = some $ some t
|