git.iko.soy/Idris-dev
on master help sign in
Substitute default args in elab scripts
0453200David Raymond Christiansen
src/Idris/AbsSyntax.hs+1
compare with master
unifiedsplit
@@ -2023,6 +2023,7 @@ substMatchShadow n shs tm t = sm shs t where
2023 sm xs (PHidden x) = PHidden (sm xs x)
2023 sm xs (PHidden x) = PHidden (sm xs x)
2024 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2024 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
2025 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2025 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
2026+ sm xs (PRunElab fc script) = PRunElab fc (sm xs script)
2026 sm xs x = x
2027 sm xs x = x
2027
2028
2028 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
2029 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))