Tidy output of :makelemma
commitdb88c3eaa10d55d9b0c773d885e78cacb4eca600
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 11 May 2014, 20:38 (12 years ago)
parentaf99a9d
CHANGELOG+2
@@ -20,6 +20,8 @@ New in 0.9.13:
2020* Totality errors are now treated as warnings until code generation time, when they become
2121 errors again. This allows users to use the interactive editing features to fix totality
2222 issues, but no programs that violate the stated assumptions will actually run.
23+* Added :makelemma command, which adds a new top level definition to solve
24+ a metavariable.
2325
2426Internal changes
2527
src/Idris/Interactive.hs+1−1
@@ -240,7 +240,7 @@ makeLemma h fn updatefile l n
240240
241241 appArgs (Bind n@(UN c) (Pi _) sc)
242242 | thead c /= '_' = " " ++ show n ++ appArgs sc
243− appArgs (Bind _ (Pi _) sc) = " " ++ appArgs sc
243+ appArgs (Bind _ (Pi _) sc) = appArgs sc
244244 appArgs _ = ""
245245
246246 stripMNBind (PPi b n@(UN c) ty sc)