Agda.TypeChecking.Rules.LHS.ProblemRest

Documentation

useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope

Rename the variables in a telescope using the names from a given pattern

noProblemRest :: Problem -> Bool

Are there any untyped user patterns left?

problemFromPats

Arguments

:: [NamedArg Pattern]

The user patterns.

-> Type

The type the user patterns eliminate.

-> TCM Problem

The initial problem constructed from the user patterns.

Construct an initial split Problem from user patterns. Example: @

Case : {A : Set} → Maybe A → Set → Set → Set Case nothing B C = B Case (just _) B C = C

sample : {A : Set} (m : Maybe A) → Case m Bool (Maybe A → Bool) sample (just a) (just b) = true sample (just a) nothing = false sample nothing = true The problem generated for the first clause of sample with patterns just a, just b would be: problemInPat = ["_", "just a"] problemOutPat = [identity-permutation, [A, "m"]] problemTel = [A : Set, m : Maybe A] problemRest = restPats = ["just b"] restType = "Case m Bool (Maybe A -> Bool)" @

updateProblemRest_ :: Problem -> TCM (Nat, Problem)

Try to move patterns from the problem rest into the problem. Possible if type of problem rest has been updated to a function type.

updateProblemRest :: LHSState -> TCM LHSState