Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fprop and ftrans can't handle match statements #16

Open
lecopivo opened this issue Aug 29, 2023 · 1 comment
Open

fprop and ftrans can't handle match statements #16

lecopivo opened this issue Aug 29, 2023 · 1 comment
Labels
bug Something isn't working fprop Tactic `fprop` that proves function properties ftrans Tactic `ftrans` for function transformation

Comments

@lecopivo
Copy link
Owner

fprop and ftrans tactics can't handle match statements

likely #15 has to be solved first

This should work

import SciLean
open SciLean

example : IsDifferentiable ℝ (fun ((x,y,z) : ℝ×ℝ×ℝ) => z) := by fprop

example 
  : (cderiv ℝ (fun ((x,y,z) : ℝ×ℝ×ℝ) => z))
    =
    fun (x,y,z) (dx,dy,dz) => dz := by ftrans only
@lecopivo lecopivo added bug Something isn't working fprop Tactic `fprop` that proves function properties ftrans Tactic `ftrans` for function transformation labels Aug 29, 2023
@lecopivo
Copy link
Owner Author

This is broken for unrelated reasons now. Investigate!

@lecopivo lecopivo reopened this Apr 22, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working fprop Tactic `fprop` that proves function properties ftrans Tactic `ftrans` for function transformation
Projects
None yet
Development

No branches or pull requests

1 participant