GitHub · Where software is built

Preview

Labels Milestones New issue

Extensional TT as formulated is not suitable for automated unification

priority: extreme

#34

· Russoul opened

on Jan 28, 2024

Reference the material that has influenced and has been used to build Nova

#33

· Russoul opened

on Jan 14, 2024

Collect all reasons why unification problem is stuck

priority: medium

scope: unification

#31

· Russoul opened

on Dec 29, 2023

Get rid of nameful meta-context in favour of a nameless one.

priority: medium

#29

· Russoul opened

on Dec 27, 2023

Design and implement a system for testing Nova

#28

· Russoul opened

on Dec 27, 2023

Figure out why `Elem` elaboration is slow and fix the issue

scope: elaboration

#26

· Russoul opened

on Dec 24, 2023

Design and implement Coquand-Russell externally indexed universe hierarchy.

scope: elaboration

scope: unification

#25

· Russoul opened

on Dec 22, 2023

Note about universes

#24

· Russoul opened

on Dec 22, 2023

Check surface path syntax for correctness before running a tactic on it

priority: medium

#19

· Russoul opened

on Dec 18, 2023

Try integrating frex into the tactics language to discharge equations

priority: medium

#18

· Russoul opened

on Dec 17, 2023

Design and implement a form of co-inductive types

scope: elaboration

scope: unification

#17

· Russoul opened

on Dec 17, 2023

Think of implementing quotient indexed W-type as it's equivalent to strictly positive quotient inductive schemas in our TT

priority: medium

scope: elaboration

scope: unification

#16

· Russoul opened

on Dec 9, 2023