Equations
- Nat.SOM.instInhabitedExpr = { default := Nat.SOM.Expr.num default }
Equations
- Nat.SOM.Expr.denote ctx (Nat.SOM.Expr.num n) = n
- Nat.SOM.Expr.denote ctx (Nat.SOM.Expr.var v) = Nat.Linear.Var.denote ctx v
- Nat.SOM.Expr.denote ctx (a.add b) = (Nat.SOM.Expr.denote ctx a).add (Nat.SOM.Expr.denote ctx b)
- Nat.SOM.Expr.denote ctx (a.mul b) = (Nat.SOM.Expr.denote ctx a).mul (Nat.SOM.Expr.denote ctx b)
Instances For
@[reducible, inline]
Equations
Instances For
Equations
Instances For
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Instances For
theorem
Nat.SOM.Expr.eq_of_toPoly_eq
(ctx : Linear.Context)
(a b : Expr)
(h : (a.toPoly == b.toPoly) = true)
: