elaboration-zoo/04-implicit-args at master · AndrasKovacs/elaboration-zoo · GitHub

Name		Name	Last commit message	Last commit date
parent directory ..
Common.hs		Common.hs
Cxt.hs		Cxt.hs
Elaboration.hs		Elaboration.hs
Errors.hs		Errors.hs
Evaluation.hs		Evaluation.hs
Main.hs		Main.hs
Metacontext.hs		Metacontext.hs
Parser.hs		Parser.hs
Presyntax.hs		Presyntax.hs
Pretty.hs		Pretty.hs
README.md		README.md
Syntax.hs		Syntax.hs
Unification.hs		Unification.hs
Value.hs		Value.hs
elabzoo-implicit-args.cabal		elabzoo-implicit-args.cabal
example.txt		example.txt
package.yaml		package.yaml
stack.yaml		stack.yaml

README.md

elabzoo-implicit-args

This package implements named implicit arguments following Agda convention and behavior, with first-class implicit dependent function types.

The implicit argument insertion is based on section 2.6 of Elaboration with first-class implicit function types, but we additionally support named implicit arguments in the style of Agda.

See example.txt for a demo of implicit insertion behavior.