diff options
Diffstat (limited to 'src/Inky/Term.idr')
| -rw-r--r-- | src/Inky/Term.idr | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr index 3c5d214..884256f 100644 --- a/src/Inky/Term.idr +++ b/src/Inky/Term.idr @@ -5,9 +5,9 @@ import public Inky.Type import Data.List.Quantifiers import Data.Singleton import Data.These -import Inky.Data.SnocList.Quantifiers -import Inky.Decidable -import Inky.Decidable.Maybe +import Flap.Data.SnocList.Quantifiers +import Flap.Decidable +import Flap.Decidable.Maybe %hide Prelude.Ops.infixl.(>=>) @@ -85,13 +85,6 @@ data NotFunction : (bound : List String) -> (a : Ty tyCtx) -> Type %name NotFunction contra export -isFunctionRecompute : - {a : Ty tyCtx} -> IsFunction bound a dom cod -> (Singleton dom, Singleton cod) -isFunctionRecompute Done = (Val _, Val _) -isFunctionRecompute (Step {a} prf) = - mapFst (\case Val _ => Val _) $ isFunctionRecompute prf - -export isFunctionUnique : IsFunction bound a dom cod -> IsFunction bound a dom' cod' -> (dom = dom', cod = cod') isFunctionUnique Done Done = (Refl, Refl) |