lecopivo/SciLean

Issues

• lsimp projection sees through let bindings

  #20 opened a year ago by lecopivo
  2

• fun prop fails to find local theorem with match

  #32 opened 3 months ago by lecopivo
  1

• LinearOrderedAddCommGroup instance for RealScalar

  #42 opened 5 months ago by lecopivo
  1

• symbol lookup error, likely due to a stack overflow or a bug.

  #41 opened 5 months ago by tribbloid
  3

• PDE Support

  #39 opened 6 months ago by Adarsh321123
  4

• inconsistent range notation

  #37 opened 7 months ago by Seasawher
  2

• can scalar have a repr instance when ground fields do?

  #36 opened 7 months ago by alok
  3

• `if_pull` tactic uses `sorry`

  #35 opened 9 months ago by lecopivo
  0

• Rules for not fully applied constants

  #9 opened a year ago by lecopivo
  1

• `fprop` and `ftrans` can't handle match statements

  #16 opened a year ago by lecopivo
  1

• `fun_trans` can't see through let bindings

  #34 opened 9 months ago by lecopivo
  0

• `fprop` can't handle fvars that are not fully applied

  #23 opened 10 months ago by lecopivo
  2

• bad bahavior of isDefEq with introElem and DataArray

  #18 opened 10 months ago by lecopivo
  2

• `ftrans` hitting maximum recursion depth

  #14 opened 10 months ago by lecopivo
  0

• `fprop` struggles with universes

  #13 opened 10 months ago by lecopivo
  2

• Custom rewrite for ftrans and improved ftrans trace

  #10 opened 10 months ago by lecopivo
  1

• Infer function property in one variable from property about multiple variables

  #8 opened 10 months ago by lecopivo
  0

• Wrong shapes generated or pretty-printed

  #31 opened a year ago by alok
  0

• replicate the really cool wavy hamiltonian pic at top and bottom

  #30 opened a year ago by alok
  0

• add lake install copy paste to top of readme

  #29 opened a year ago by alok
  0

• command to generate linear map

  #27 opened a year ago by lecopivo
  0

• `lsimp` is not fully normalizing let bindings through application

  #26 opened a year ago by lecopivo
  0

• `ftrans` applies incorrect rule

  #25 opened a year ago by lecopivo
  0

• `#generate_revCDeriv` generates incorrect name

  #24 opened a year ago by lecopivo
  0

• unification issue with overly applied constant

  #22 opened a year ago by lecopivo
  0

• universe issues in `semiAdjoint.pi_rule`

  #21 opened a year ago by lecopivo
  0

• `ftrans` unfold let bindings sometimes

  #19 opened a year ago by lecopivo
  0

• `let_normalize` unfolds `fwdCDeriv`

  #17 opened a year ago by lecopivo
  0

• `fprop` and `ftrans` can't handle `Expr.proj`

  #15 opened a year ago by lecopivo
  0

• new attribute `ftrans_unfold`

  #12 opened a year ago by lecopivo
  0

• Broken link

  #11 opened a year ago by joaquimpuig
  3

• Dimensions

  #5 opened 2 years ago by reubenharry
  1

• Mechanics.olean not building?

  #1 opened 3 years ago by omrischwarz
  3