diff options
Diffstat (limited to 'src/Data/Term.idr')
| -rw-r--r-- | src/Data/Term.idr | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Data/Term.idr b/src/Data/Term.idr index 2afc774..3b16f38 100644 --- a/src/Data/Term.idr +++ b/src/Data/Term.idr @@ -38,6 +38,13 @@ public export 0 (.=.) : Rel (Fin k -> Term sig n) f .=. g = (i : Fin k) -> f i = g i +export +subCong : {f, g : Fin k -> Term sig n} -> f .=. g -> (t : Term sig k) -> f <$> t = g <$> t +subCong prf (Var i) = prf i +subCong prf (Op op ts) = + cong (Op op) $ + mapExtensional (f <$>) (g <$>) (\t => subCong prf (assert_smaller ts t)) ts + -- Substitution is Monadic ----------------------------------------------------- export @@ -80,6 +87,10 @@ opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n opInjectiveLen Refl = Refl export +opInjectiveTs' : {0 ts, us : Vect k (Term sig n)} -> (prf : Op op ts = Op op us) -> ts = us +opInjectiveTs' Refl = Refl + +export opInjectiveTs : {0 ts : Vect k (Term sig n)} -> {0 us : Vect j (Term sig n)} -> |