Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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

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

noProblemRest :: Problem -> Bool Source

Are there any untyped user patterns left?

problemFromPats Source


:: [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) Source

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