Agda-2.5.1.2: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Rules.LHS.ProblemRest

Synopsis

# Documentation

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

Are there any untyped user patterns left?

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 = [A, "m"] problemTel = [A : Set, m : Maybe A] problemRest = restPats = ["just b"] restType = "Case m Bool (Maybe A -> Bool)" @

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