git.iko.soy/Idris-dev
on master help sign in
Fix reverse elaboration of dependent pairs
fee6b51Edwin Brady
src/Core/CoreParser.hs+1−1
compare with master
unifiedsplit
@@ -23,7 +23,7 @@ idrisDef = haskellDef {
23 "do", "dsl", "import", "impossible",
23 "do", "dsl", "import", "impossible",
24 "case", "of", "total",
24 "case", "of", "total",
25 "infix", "infixl", "infixr",
25 "infix", "infixl", "infixr",
26− "where", "with", "forall", "syntax", "proof",
26+ "where", "with", "syntax", "proof",
27 "using", "params", "namespace", "class", "instance",
27 "using", "params", "namespace", "class", "instance",
28 "public", "private", "abstract",
28 "public", "private", "abstract",
29 "Int", "Integer", "Float", "Char", "String", "Ptr"]
29 "Int", "Integer", "Float", "Char", "String", "Ptr"]
src/Idris/Delaborate.hs+1−1
@@ -50,7 +50,7 @@ delab' ist tm fullname = de [] tm
50 deFn env (P _ n _) [ty, Bind x (Lam _) r]
50 deFn env (P _ n _) [ty, Bind x (Lam _) r]
51 | n == UN "Exists"
51 | n == UN "Exists"
52 = PDPair un (PRef un x) (de env ty)
52 = PDPair un (PRef un x) (de env ty)
53− (de env (instantiate (P Bound x ty) r))
53+ (de ((x,x):env) (instantiate (P Bound x ty) r))
54 deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)
54 deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)
55 | n == eqTy = PEq un (de env l) (de env r)
55 | n == eqTy = PEq un (de env l) (de env r)
56 | n == UN "Ex_intro" = PDPair un (de env l) Placeholder
56 | n == UN "Ex_intro" = PDPair un (de env l) Placeholder