Search results

Add UInt* byte seq instances

Status: Open.

#36 In JamesGallicchio/LeanColls;

· JamesGallicchio opened on May 3, 2024

Add String implementations

enhancementNew feature or requestNew feature or request

Status: Open.

#35 In JamesGallicchio/LeanColls;

· JamesGallicchio opened on May 3, 2024

Add ofFnM

enhancementNew feature or requestNew feature or request

good first issueGood for newcomersGood for newcomers

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#34 In JamesGallicchio/LeanColls;

· JamesGallicchio opened on May 1, 2024

Split LeanColls/Classes/Ops.lean

chore

Status: Open.

#29 In JamesGallicchio/LeanColls;

· JamesGallicchio opened on Apr 17, 2024

Index.card has an extra universe parameter

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#27 In JamesGallicchio/LeanColls;

· JamesGallicchio opened on Mar 28, 2024

Map operation class

bikeshedNamespace issuesNamespace issues

enhancementNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#25 In JamesGallicchio/LeanColls;

· JamesGallicchio opened on Mar 14, 2024

Elab issues with index notation

bugSomething isn't workingSomething isn't working

Status: Open.

#22 In JamesGallicchio/LeanColls;

· lecopivo opened on Mar 8, 2024

reduce and family

enhancementNew feature or requestNew feature or request

Status: Open.

#4 In JamesGallicchio/LeanColls;

· JamesGallicchio opened on Jan 18, 2024

Dependently typed Indexed

enhancementNew feature or requestNew feature or request

Status: Open.

#2 In JamesGallicchio/LeanColls;

· lecopivo opened on Jan 17, 2024