-
Notifications
You must be signed in to change notification settings - Fork 14
Issues
is:issue state:open
is:issue state:open
Issue creation is restricted in this repository
Search results
Proof assistant test: structure identity principle for magmas
C-metaComponent: user-facing notation, typechecker, tacticsComponent: user-facing notation, typechecker, tacticsD-lowDifficulty: lowDifficulty: lowI-highImpact: highImpact: highStatus: Open.#165 In sinhp/HoTTLean;Unstructured Id iff Structured Id
C-modelComponent: abstract model (natural or unstructured)Component: abstract model (natural or unstructured)Status: Open.#158 In sinhp/HoTTLean;- Status: Open.#157 In sinhp/HoTTLean;
Beck-chevalley for pi-clans
C-modelComponent: abstract model (natural or unstructured)Component: abstract model (natural or unstructured)Status: Open.#156 In sinhp/HoTTLean;Improved mutual induction
C-metaComponent: user-facing notation, typechecker, tacticsComponent: user-facing notation, typechecker, tacticsD-highDifficulty: highDifficulty: highI-lowImpact: lowImpact: lowStatus: Open.#155 In sinhp/HoTTLean;Look for redundancy in typing rules
C-syntaxComponent: typing rules, interpretation functionComponent: typing rules, interpretation functionD-unkDifficulty: unknownDifficulty: unknownI-lowImpact: lowImpact: lowStatus: Open.#154 In sinhp/HoTTLean;pi-clan refactor general semantics
C-modelComponent: abstract model (natural or unstructured)Component: abstract model (natural or unstructured)Status: Open.#149 In sinhp/HoTTLean;Pi-clan polynomials
D-highDifficulty: highDifficulty: highI-critImpact: criticalImpact: criticalO-polyOther: improvements to PolyOther: improvements to PolyStatus: Open.#148 In sinhp/HoTTLean;pi-clans refactor
C-grpdComponent: groupoid modelComponent: groupoid modelC-modelComponent: abstract model (natural or unstructured)Component: abstract model (natural or unstructured)C-syntaxComponent: typing rules, interpretation functionComponent: typing rules, interpretation functionD-highDifficulty: highDifficulty: highI-critImpact: criticalImpact: criticalO-polyOther: improvements to PolyOther: improvements to PolyStatus: Open.#145 In sinhp/HoTTLean;Support level polymorphism
C-metaComponent: user-facing notation, typechecker, tacticsComponent: user-facing notation, typechecker, tacticsI-highImpact: highImpact: highStatus: Open.#143 In sinhp/HoTTLean;Typechecker optimization
C-metaComponent: user-facing notation, typechecker, tacticsComponent: user-facing notation, typechecker, tacticsI-critImpact: criticalImpact: criticalO-groupOther: issue groupOther: issue groupO-helpHelp wantedHelp wantedStatus: Open.#142 In sinhp/HoTTLean;Get rid of level annotations on terms
C-syntaxComponent: typing rules, interpretation functionComponent: typing rules, interpretation functionD-lowDifficulty: lowDifficulty: lowI-lowImpact: lowImpact: lowStatus: Open.#119 In sinhp/HoTTLean;