fee6b51 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix reverse elaboration of dependent pairs

commitfee6b51e556a6d2230221556347928b8a5ee4bee authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 30 Apr 2012, 15:58 (14 years ago) parent126eb94

2 files changed+2−2

unifiedsplit

src/Core/CoreParser.hs+1−1

@@ -23,7 +23,7 @@ idrisDef = haskellDef {

2323 "do", "dsl", "import", "impossible",

2424 "case", "of", "total",

2525 "infix", "infixl", "infixr",

26− "where", "with", "forall", "syntax", "proof",

26+ "where", "with", "syntax", "proof",

2727 "using", "params", "namespace", "class", "instance",

2828 "public", "private", "abstract",

2929 "Int", "Integer", "Float", "Char", "String", "Ptr"]

src/Idris/Delaborate.hs+1−1

@@ -50,7 +50,7 @@ delab' ist tm fullname = de [] tm

5050 deFn env (P _ n _) [ty, Bind x (Lam _) r]

5151 | n == UN "Exists"

5252 = 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))

5454 deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)

5555 | n == eqTy = PEq un (de env l) (de env r)

5656 | n == UN "Ex_intro" = PDPair un (de env l) Placeholder