mortberg/cubicaltt

Issues

• Doesn't work on M1 Mac

  #122 opened a year ago by iho
  0

• Add command-line options to run commands (or take a command file) and/or redirect output

  #103 opened 2 years ago by favonia
  7

• Problem with parser generated by bnfc

  #118 opened 4 years ago by wmacmil
  4

• cubical.exe does not support {- -} comments

  #104 opened 6 years ago by mwand
  2

• boundaries of nested splits

  #102 opened 6 years ago by dlicata335
  1

• New lines when printing systems

  #101 opened 6 years ago by guillaumebrunerie
  3

• Add support for nested mutual blocks again

  #48 opened 8 years ago by mortberg
  6

• Etale Map

  #98 opened 6 years ago by 5HT
  4

• Hopf Fibration

  #97 opened 6 years ago by 5HT
  12

• missing dependencies of experiments/truncS2.ctt

  #92 opened 6 years ago by nponeccop
  1

• Parser error messages are truncated too much

  #95 opened 6 years ago by necrosovereign
  5

• Solution at "hard" exercise at lecture2.ctt

  #73 opened 7 years ago by xekoukou
  2

• Evaluation priority idea

  #93 opened 7 years ago by PaulGustafson
  0

• Path completion in :l

  #91 opened 7 years ago by nponeccop
  0

• Layout errors crash REPL

  #90 opened 7 years ago by nponeccop
  0

• Allow opaque/transparent in the command line

  #89 opened 7 years ago by guillaumebrunerie
  0

• Does indent matter in cubicaltt?

  #87 opened 7 years ago by 1-p
  4

• Bracket matching of \(x : A)

  #84 opened 7 years ago by guillaumebrunerie
  1

• Document opaque / transparent

  #85 opened 7 years ago by joelburget
  1

• A pattern matching for predicate function

  #83 opened 7 years ago by xgrommx
  5

• Bound Check Error

  #82 opened 7 years ago by 5HT
  1

• Useless(?) hComp’s with empty systems when using higher inductive types

  #67 opened 7 years ago by guillaumebrunerie
  10

• Syntax highlighting for all keywords

  #61 opened 7 years ago by mortberg
  1

• cubicaltt crashes when replacing an 'undefined' with a 'hole'.

  #74 opened 7 years ago by xekoukou
  0

• Please don't call it the "grad lemma".

  #72 opened 7 years ago by mikeshulman
  6

• Spurious error with incorrect import

  #64 opened 7 years ago by jonsterling
  2

• Learning Guide

  #57 opened 7 years ago by ronaldpetty
  2

• "forwardHIT: neutral b" error in hit branch, but not master

  #69 opened 7 years ago by PaulGustafson
  1

• Print a warning when a name is shadowed

  #43 opened 7 years ago by mortberg
  3

• Nested splits and path constructors

  #63 opened 7 years ago by IanOrton
  2

• Issue with HIT path constructors.

  #47 opened 8 years ago by RafaelBocquet
  3

• Definitional equality of lambda is wrong?

  #53 opened 8 years ago by molikto
  2

• Add Identity types

  #42 opened 8 years ago by mortberg
  4

• Conversion bug with glue systems?

  #52 opened 8 years ago by tomjack
  1

• Wired program type checked.

  #51 opened 8 years ago by molikto
  1

• Type-checking performance issues

  #38 opened 8 years ago by gullcomb
  3

• Renaming

  #41 opened 8 years ago by mortberg
  1

• Canonicity failure for Z from recursive path constructors

  #35 opened 9 years ago by tomjack
  6

• Origin of type errors

  #22 opened 9 years ago by abooij
  1

• Constructors as first-class citizen

  #16 opened 9 years ago by abooij
  2

• Maintain semantics of type signatures

  #25 opened 8 years ago by abooij
  2

• List reserved names

  #37 opened 8 years ago by abooij
  1

• Composing with refl gives different path

  #28 opened 9 years ago by abooij
  2

• Finish the proof that \pi_4(S^3)=Z/2Z?

  #33 opened 9 years ago by markfarrell
  0

• The n-th homotopy group of the n-sphere is the integers?

  #31 opened 9 years ago by markfarrell
  0

• The total space of the Hopf fibration, as well as the join of two 1-spheres, is the 3-sphere?

  #34 opened 9 years ago by markfarrell
  0

• Eilenberg-MacLane Spaces?

  #32 opened 9 years ago by markfarrell
  0

• Path from the loop space of the torus to the product of two circles?

  #30 opened 9 years ago by markfarrell
  0

• Incorrect pattern matching in the type checker makes bottom provable

  #27 opened 9 years ago by abooij
  2

• univalence normalization

  #26 opened 9 years ago by stelleg
  21