diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-07-03 18:21:50 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-07-03 18:21:50 +0100 |
| commit | 9039055d9a994bde34e0c0bfedad1a72cd9c17a7 (patch) | |
| tree | d9a843875ee25b64797e56889a8788b7910afde5 /src/Term/Semantics.idr | |
| parent | 6385ecf96cd60885c221e3144b5a5ec63eb5c831 (diff) | |
Add literals as primitive term.
Diffstat (limited to 'src/Term/Semantics.idr')
| -rw-r--r-- | src/Term/Semantics.idr | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr index 2e61040..e8424f2 100644 --- a/src/Term/Semantics.idr +++ b/src/Term/Semantics.idr @@ -49,7 +49,7 @@ fullSem' (App (MakePair t u _)) = do t <- sem' t u <- sem' u pure (\ctx => t ctx (u ctx)) -fullSem' Zero = pure (const 0) +fullSem' (Lit n) = pure (const n) fullSem' (Suc t) = do t <- fullSem' t pure (S . t) |