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