Agda.TypeChecking.Primitive

buildList A ts builds a list of type List A. Assumes that the terms ts all have type A.

Used for both primForce and primForceLemma.

Get the ArgInfo of the principal argument of BUILTIN REFL.

Returns Nothing for e.g. data Eq {a} {A : Set a} (x : A) : A → Set a where refl : Eq x x

Returns Just ... for e.g. data Eq {a} {A : Set a} : (x y : A) → Set a where refl : ∀ x → Eq x x

Converts MetaIds to natural numbers.

mkPrimInjective takes two Set0 a and b and a function f of type a -> b and outputs a primitive internalizing the fact that f is injective.