JetBrains arend-lib issues

JetBrains / arend-lib

Apache License 2.0

79 stars 23 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Regular monomorphisms are stable under pullbacks

#72 bakinovsky-m opened 2 weeks ago
0
Not intuitive error message of mcases tactic.

#71 sxhya opened 1 month ago
0
Representation

#70 s3midetnov closed 4 weeks ago
0
Representation

#69 s3midetnov closed 3 months ago
1
Representation

#68 s3midetnov closed 3 months ago
0
Presheaves and Yoneda Lemma

#67 FeorgeGeorge opened 4 months ago
0
Is this a typo?

#66 ice1000 closed 3 weeks ago
0
quotient universal property

#65 s3midetnov closed 3 months ago
0
Toposes and Heyting Algebras

#64 FeorgeGeorge closed 4 months ago
0
universal group quotient, gset definition

#63 s3midetnov closed 6 months ago
0
Group upd

#62 s3midetnov closed 7 months ago
0
Make composition operator o infix

#61 s3midetnov opened 7 months ago
0
Fix replaceSubexpressions

#60 part-xx closed 1 year ago
0
Prove a characterization of homogeneous ideals

#58 valis closed 1 year ago
0
Prove a lemma about homogeneous decomposition

#57 valis closed 1 year ago
3
Create FiniteMultiset.ard

#56 ice1000 opened 1 year ago
0
Define T3

#55 ice1000 opened 1 year ago
0
Finish the construction of the structure of a field on reals

#54 valis closed 3 months ago
0
Improve instance search in `equation`

#53 valis opened 2 years ago
0
Proven that the radical of the ideal generated by two elements is equal to the radical of the ideal generated by powers of these elements

#52 TurtlePU closed 2 years ago
1
Proven that the ideal generated by a two-element set consists of linear combinations of those elements

#51 TurtlePU closed 2 years ago
2
Fix sigma parameters creation in arend-lib

#50 knisht closed 2 years ago
0
Prove that a weakly regular locale is weakly Hausdorff

#49 valis opened 2 years ago
0
Prove that open maps of locales are closed under composition

#48 valis opened 2 years ago
0
Prove that strongly dense maps are closed under pullbacks along open maps

#47 valis opened 2 years ago
0
Prove that open maps of locales are closed under pullbacks

#46 valis opened 2 years ago
0
Show that the pullback of regular monomorphisms is their meet in the preorder of regular subojects

#45 valis opened 2 years ago
0
Prove that regular monomorphisms are stable under pullbacks

#44 valis opened 2 years ago
0
Prove that the ideal generated by a two-element set consists of linear combinations of those elements

#43 valis closed 2 years ago
1
Show that the forgetful functor from rings to sets creates limits

#42 valis opened 2 years ago
0
Prove that the radical of the ideal generated by two elements is equal to the radical of the ideal generated by powers of these elements

#41 valis closed 2 years ago
1
Show that the spectrum of a ring is locally ringed

#40 valis closed 1 year ago
0
Extend `run` meta to support trailing lambdas

#39 TurtlePU opened 2 years ago
1
Add Term Rewriting Systems

#38 knisht closed 2 years ago
0
Refactor: fix "Redundant parentheses" warnings

#37 marat-rkh closed 2 years ago
0
Refactor: fix "Redundant parentheses" warnings

#36 marat-rkh closed 3 years ago
0
Add metas for \Pi, similar to metas for \Sigma

#35 marat-rkh closed 2 years ago
3
'cases' meta

#34 valis closed 3 years ago
0
Potential typo

#33 ice1000 closed 3 years ago
0
Upgrade gradle (jetbrains/arend#277)

#32 ice1000 closed 3 years ago
0
Put annotation on the correct place

#31 ice1000 closed 3 years ago
0
Allow additional arguments for \case in mcases

#30 valis closed 3 years ago
0
Generalize the definition of Subset

#29 tonyxty opened 3 years ago
0
Simply Torus proofs with mcases

#28 ice1000 closed 3 years ago
0
Meta `mcases` throws exception

#27 ice1000 closed 4 years ago
0
Compute the context in the equation meta only once

#26 valis opened 4 years ago
0
Feature request: automatically generate "equals" definitions

#25 tonyxty closed 3 years ago
1
Compile Java with utf-8

#24 ice1000 closed 4 years ago
0
Adapt latest literal checker API

#23 ice1000 closed 4 years ago
0
Workaround github actions, improve build.gradle.kts

#22 ice1000 closed 4 years ago
0