Agda snippets

agda.json

{
	"set type": {
		"prefix": "se",
		"body": "Set ${1|ℓ,ℓ₁,ℓ₂,ℓᵢ,ℓⱼ,lsuc ?,lzero|}",
		"description": "Set type"
	},
	"Type type": {
		"prefix": "ty",
		"body": "Type ${1|ℓ,ℓ₁,ℓ₂,ℓᵢ,ℓⱼ,lsuc ?,lzero|}",
		"description": "Type type"
	},
	"data types": {
		"prefix": "da",
		"body": "\ndata\n  ${1:typeName} ${2:parameters}\n   : ${3|Set,Type|} ${4|ℓ,ℓ₁,ℓ₂,ℓᵢ,ℓⱼ,lsuc ?,lzero|}\n  where\n  ${5:constructor-name} : $6",
		"description": "data type"
	},
	"with-abstraction": {
		"prefix": "wi",
		"body": "\n with {! $1 !}\n... | {! $2 !} = {! $3 !}",
		"description": "with abstraction"
	},
	"equation-reasoning": {
		"prefix": "be",
		"body": "\n  begin\n  {! $1 !}\n  ≡⟨ {! $2 !} ⟩\n  {! $3 !}\n  ∎",
		"description": "equational reasoning"
	},
	"equation-reasoning-step": {
		"prefix": "st",
		"body": "  ≡⟨ {! $2 !} ⟩\n{! $3 !}",
		"description": "step equational reasoning"
	},
	"record types": {
		"prefix": "re",
		"body": "\nrecord\n  $1\n   : $2\n  where\n  constructor $3\n  field\n  $4 : $5",
		"description": "record type"
	},
	"lemma": {
		"prefix": ["lem","def","the"],
		"body": "\n$1\n  : {! $2 !}\n$1 = {! $3 !}",
		"description": "Def lemma."
	},
	"postulate": {
		"prefix": "po",
		"body": "postulate\n  $1 : {! $2 !}",
		"description": "Postulate"
	},
	"variable": {
		"prefix": "va",
		"body": "variable\n  $1 : {! $2 !}",
		"description": "Variable"
	},
		"comment type 1": {
			"prefix": "co",
			"body": "{-\n\t$1\n-}",
			"description": "comment"
		},
		"module": {
			"prefix": "mo",
			"body": "\nmodule\n  ${1:nameModule}\n  where\n  ",
			"description": "module type"
		}
}