diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-22 17:57:48 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-22 17:57:48 +0100 |
| commit | 6385ecf96cd60885c221e3144b5a5ec63eb5c831 (patch) | |
| tree | 541d06feb1517e91f62ab60854b80bb29343784c /src/Encoded/Arith.idr | |
| parent | 0ddaf1b2c9ca66cf0ae03d2f6ad792c7885dfc32 (diff) | |
Add encodings for containers.
Remove useless junk.
Diffstat (limited to 'src/Encoded/Arith.idr')
| -rw-r--r-- | src/Encoded/Arith.idr | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/src/Encoded/Arith.idr b/src/Encoded/Arith.idr index d2f83bc..fe9bc68 100644 --- a/src/Encoded/Arith.idr +++ b/src/Encoded/Arith.idr @@ -32,10 +32,15 @@ pred = Abs' (\n => App (Rec n (Const Zero) - (Abs' (\f => - Rec (App f [<Zero]) - (Abs' (\k => Rec k (Suc Zero) (Const Zero))) - (Const $ Abs' (\k => Rec k (Suc Zero) (Abs' Suc . shift f)))))) + (Abs $ Abs $ + let f = Var (There Here) in + let k = Var Here in + Rec k + (Lit 1) + (Const $ + Rec (App f [<Zero]) + Zero + (Const $ Suc $ App f [<Lit 1])))) [<Lit 1]) export @@ -76,6 +81,6 @@ divmod = Abs $ Abs $ (App pair [<Zero, Zero]) (Abs' (\p => App if' - [<App lte [<shift d, App snd [<p]] + [<App lte [<shift d, Suc (App snd [<p])] , App pair [<Suc (App fst [<p]), Zero] , App mapSnd [<Abs' Suc, p]])) |