Merge pull request #3067 from ahmadsalim/fix/sensibledependentpair
Use type/term pun gotten from parsing to elaborate dependent pairs
commit716b6a0be40d65388e4661fca85a05528ef368e9
authorDavid Christiansen <david@davidchristiansen.dk>
dateMon 28 Mar 2016, 16:16 (11 years ago)
parentba53b91e60a749
src/Idris/Elab/Term.hs+4−3
@@ -413,14 +413,15 @@ elab ist info emode opts fn tm
413413 pimp (sUN "B") Placeholder False,
414414 pexp l, pexp r])
415415 elab' ina _ (PDPair fc hls p l@(PRef nfc hl n) t r)
416− = case t of
417− Placeholder ->
416+ = case p of
417+ IsType -> asType
418+ IsTerm -> asValue
419+ TypeOrTerm ->
418420 do hnf_compute
419421 g <- goal
420422 case g of
421423 TType _ -> asType
422424 _ -> asValue
423− _ -> asType
424425 where asType = elab' ina (Just fc) (PApp fc (PRef NoFC hls sigmaTy)
425426 [pexp t,
426427 pexp (PLam fc n nfc Placeholder r)])