Search results

DECapitalize

Status: Open.

#222 In leanprover-community/mathport;

· jcommelin opened on Jan 20, 2023

double #align with toAdditive to existing definition

Status: Open.

#221 In leanprover-community/mathport;

· rwbarton opened on Jan 19, 2023

mathport sometimes panics

Status: Open.

#220 In leanprover-community/mathport;

· rwbarton opened on Jan 19, 2023

Theorem names beginning with _root_ are not properly translated

Status: Open.

#210 In leanprover-community/mathport;

· winstonyin opened on Dec 11, 2022

Notations no longer work in binport

Status: Open.

#192 In leanprover-community/mathport;

· gebner opened on Oct 26, 2022

Extreme runtime increase

Status: Open.

#172 In leanprover-community/mathport;

· gebner opened on Aug 26, 2022

Accidentally recursive definitions

Status: Open.

#168 In leanprover-community/mathport;

· gebner opened on Aug 24, 2022

tt is sometimes not translated

bugSomething isn't workingSomething isn't working

Status: Open.

#167 In leanprover-community/mathport;

· gebner opened on Aug 24, 2022

dot-notation is often omitted

bugSomething isn't workingSomething isn't working

Status: Open.

#166 In leanprover-community/mathport;

· gebner opened on Aug 23, 2022

Translate local notation with (priority := high)

Status: Open.

#162 In leanprover-community/mathport;

· gebner opened on Aug 18, 2022

Impossible intermediate_field.adjoin notation

bugSomething isn't workingSomething isn't working

Status: Open.

#159 In leanprover-community/mathport;

· gebner opened on Aug 15, 2022

Localized notation is not scoped in binport

Status: Open.

#143 In leanprover-community/mathport;

· gebner opened on Apr 29, 2022