diff options
Diffstat (limited to 'src/Data/Term.idr')
| -rw-r--r-- | src/Data/Term.idr | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/Data/Term.idr b/src/Data/Term.idr index 01de5d2..4bb787f 100644 --- a/src/Data/Term.idr +++ b/src/Data/Term.idr @@ -22,6 +22,10 @@ public export sig .Op = Exists sig.Operator public export +interface DecOp (0 sig : Signature) where + decOp : (op, op' : sig.Op) -> Dec (op = op') + +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 @@ -45,7 +49,7 @@ export pure : (SFin k -> SFin n) -> SFin k -> Term sig n pure r = Var' . r -export +public export (<$>) : (SFin k -> Term sig n) -> Term sig k -> Term sig n f <$> Var i = f i f <$> Op op ts = Op op (map (\t => f <$> assert_smaller ts t) ts) @@ -65,7 +69,7 @@ subCong prf (Op op ts) = -- Substitution is Monadic ----------------------------------------------------- -export +public export (.) : (SFin k -> Term sig n) -> (SFin j -> Term sig k) -> SFin j -> Term sig n f . g = (f <$>) . g @@ -93,8 +97,8 @@ subAssoc f g (Op op ts) = cong (Op op) $ Calc $ export subComp : - (f : SFin (S k) -> Term sig n) -> - (r : SFin j -> SFin (S k)) -> + (f : SFin k -> Term sig n) -> + (r : SFin j -> SFin k) -> f . pure r .=. f . r subComp f r i = Refl |