# Glossary

a | b | c | d | f | i | l | o | p | r | s | t | w
 a attribute alpha-convertible algebraic universe b branching backtracking backtracking point c command convertible d de Bruijn criterion f flag first success i inhabited l left associative o option p prelude proposition r right associative s standard library sentence sort strict proposition t term type tactic table w well-typed witness