Lambda.idr

module Lambda

%default total

data Ty = TyFunc Ty Ty | TyNat

data Context = Empty | Extend Context Ty

data Contains : Context -> Ty -> Type where
  Here : Contains (Extend g ty) ty
  There : (rest :  Contains g ty)
       -> Contains (Extend g not_ty) ty

data Term : Context -> Ty -> Type where
  Var : (idx : Contains g ty)
     -> Term g ty

  Func : (body : Term (Extend g tyA) tyB)
      -> Term g (TyFunc tyA tyB)

  App : (func : Term g (TyFunc tyA tyB))
     -> (var  : Term g tyA)
     -> Term g tyB

  Zero : Term g TyNat

  Next : (inner : Term g TyNat)
      -> Term g TyNat

  Case : (scrutinee : Term g TyNat)
      -> (zero : Term g tyA)
      -> (next : Term (Extend g TyNat) tyA)
      -> Term g tyA

  Plus : Term g TyNat
      -> Term g TyNat
      -> Term g TyNat

  Rec : (body : Term (Extend g tyA) tyA)
    -> Term g tyA

term : Term Empty
            (TyFunc TyNat -- (Var Here) -
                    (TyFunc TyNat -- (Var (There Here)) -
                            (TyFunc TyNat -- (Var (There (There Here))) -
                                    (TyFunc TyNat -- (Var (There (There (There Here)))) -
                                           (TyFunc TyNat -- (Var (There (There (There (There Here))))) -
                                                   (TyFunc TyNat -- (Var (There (There (There (There (There Here)))))) -
                                                           (TyFunc TyNat -- (Var (There (There (There (There (There (There Here)))))))
                                                                   TyNat
                                                                   )
                                                                   )
                                                                   )
                                                                   )
                                                                   )
                                                                   )
                                                                   )
term =
  Func
      (Func
           (Func
                (Func
                     (Func
                          (Func
                               (Func
                                    (Func (Plus (Var Here)
                                                (Plus (Var (There Here))
                                                      (Plus (Var (There (There Here)))
                                                            (Plus (Var (There (There (There Here))))
                                                                  (Plus (Var (There (There (There (There Here)))))
                                                                        (Plus  (Var (There (There (There (There (There Here))))))
                                                                               (Var (There (There (There (There (There (There Here)))))))
                                                                        )
                                                                  )
                                                            )
                                                      )
                                                 )
                                          )
                                    )
                               )
                          )
                     )
                )
            )
       )

output.txt

1/1: Building Lambda (Lambda.idr)
TIMING Parsing Lambda.idr: 110.247s
TIMING Reading imports: 0.032s
TIMING Processing decls: 0.004s
TIMING Compile defs: 0.000s
TIMING Elaborating Lambda.idr: 110.285s
Lambda.idr:59:3--86:1:While processing right hand side of term at Lambda.idr:58:1--86:1:
When unifying Term ?g (TyFunc ?tyA (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat)))))))) and Term Empty (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat)))))))
Mismatch between:
	TyFunc TyNat TyNat
and
	TyNat
at:
59	  Func
60	      (Func
61	           (Func
62	                (Func
63	                     (Func
64	                          (Func
65	                               (Func
66	                                    (Func (Plus (Var Here)
67	                                                (Plus (Var (There Here))
68	                                                      (Plus (Var (There (There Here)))
69	                                                            (Plus (Var (There (There (There Here))))
70	                                                                  (Plus (Var (There (There (There (There Here)))))
71	                                                                        (Plus  (Var (There (There (There (There (There Here))))))
72	                                                                               (Var (There (There (There (There (There (There Here)))))))
73	                                                                        )
74	                                                                  )
75	                                                            )
76	                                                      )
77	                                                 )
78	                                          )
79	                                    )
80	                               )
81	                          )
82	                     )
83	                )
84	            )
85	       )

TIMING Build deps: 110.291s
TIMING Loading main file: 110.292s