diff options
Diffstat (limited to 'src/Data/Term.idr')
| -rw-r--r-- | src/Data/Term.idr | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/Data/Term.idr b/src/Data/Term.idr index ebb7b00..b65859e 100644 --- a/src/Data/Term.idr +++ b/src/Data/Term.idr @@ -1,7 +1,8 @@ module Data.Term -import public Data.Vect +import public Data.DPair import public Data.Fin.Strong +import public Data.Vect import Data.Vect.Properties.Map import Syntax.PreorderReasoning @@ -16,6 +17,10 @@ record Signature where %name Signature sig public export +(.Op) : Signature -> Type +sig .Op = Exists sig.Operator + +public export data Term : Signature -> Nat -> Type where Var : SFin (S n) -> Term sig (S n) Op : sig.Operator k -> Vect k (Term sig n) -> Term sig n @@ -99,6 +104,12 @@ opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n opInjectiveLen Refl = Refl export +opInjectiveOp : + (prf : Op {sig, k} op ts = Op {sig, k = n} op' us) -> + the sig.Op (Evidence k op) = Evidence n op' +opInjectiveOp Refl = Refl + +export opInjectiveTs' : {0 ts, us : Vect k (Term sig n)} -> (prf : Op op ts = Op op us) -> ts = us opInjectiveTs' Refl = Refl |