refactor(kernel/type_checker): improve ensure_pi and ensure_sort APIs

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/converter): remove unnecessary exception

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean): remove m_pos field from parameter object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/converter): relax is_def_eq test, for example is_def_eq(f(?m1), a) should generate a constraint instead of returning an error

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add 'using' syntax sugar for adding expressions to the goal's context

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): flip definition modifiers position, now they must occur after the identifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add '[fact]' modifier for 'have' expression

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add 'then have' expression

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add 'moreover have' expression

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

Conflicts:
	src/library/elaborator/elaborator.h