diff options
Diffstat (limited to 'src/Inky/Term/Checks.idr')
| -rw-r--r-- | src/Inky/Term/Checks.idr | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr index 402f623..829561a 100644 --- a/src/Inky/Term/Checks.idr +++ b/src/Inky/Term/Checks.idr @@ -204,6 +204,7 @@ fallbackCheck prf p a = (either (EmbedNC1 prf) (\xPrf => uncurry (EmbedNC2 prf) $ snd xPrf)) $ (b := p) >=> alpha b a +export synths : (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) -> (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) -> |