Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.ReconstructParameters

Description

Reconstruct dropped parameters from constructors. Used by with-abstraction to avoid ill-typed abstractions (#745). Note that the term is invalid after parameter reconstruction. Parameters need to be dropped again before using it.

Documentation