@@ -18,10 +18,10 @@ import Debug.Trace
1818
1919import Control.Monad.State.Strict
2020
21−-- Generate a pattern from an 'impossible' LHS. (Need this to eliminate the
22−-- pattern clauses which have been provided explicitly from new clause
23−-- generation.)
24−
21+-- | Generate a pattern from an 'impossible' LHS.
22+--
23+-- We need this to eliminate the pattern clauses which have been
24+-- provided explicitly from new clause generation.
2525mkPatTm :: PTerm -> Idris Term
2626mkPatTm t = do i <- getIState
2727 let timp = addImpl' True [] [] i t
@@ -44,13 +44,12 @@ mkPatTm t = do i <- getIState
4444 deNS (PRef f (NS n _)) = PRef f n
4545 deNS t = t
4646
47−-- Given a list of LHSs, generate a extra clauses which cover the remaining
48−-- cases. The ones which haven't been provided are marked 'absurd' so that the
49−-- checker will make sure they can't happen.
50−
47+-- | Given a list of LHSs, generate a extra clauses which cover the remaining
48+-- cases. The ones which haven't been provided are marked 'absurd' so
49+-- that the checker will make sure they can't happen.
50+--
5151-- This will only work after the given clauses have been typechecked and the
5252-- names are fully explicit!
53−
5453genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
5554genClauses fc n xs given
5655 = do i <- getIState