src/Encoded/Bool.idr


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

module Encoded.Bool

import Term.Syntax

export
B : Ty
B = N

export
True : Term B ctx
True = Lit 0
  
export
False : Term B ctx
False = Lit 1

export
if' : Term (B ~> ty ~> ty ~> ty) ctx
if' = Abs' (\b =>
  Rec b
    (Abs $ Const $ Var Here)
    (Const $ Const $ Abs $ Var Here))