Documentation
Init
.
Data
.
Nat
.
SOM
Search
return to top
source
Imports
Init.Data.List.BasicAux
Init.Data.Nat.Linear
Imported by
Nat
.
SOM
.
Expr
Nat
.
SOM
.
instInhabitedExpr
Nat
.
SOM
.
Expr
.
denote
Nat
.
SOM
.
Mon
Nat
.
SOM
.
Mon
.
denote
Nat
.
SOM
.
Mon
.
mul
Nat
.
SOM
.
Mon
.
mul
.
go
Nat
.
SOM
.
Poly
Nat
.
SOM
.
Poly
.
denote
Nat
.
SOM
.
Poly
.
add
Nat
.
SOM
.
Poly
.
add
.
go
Nat
.
SOM
.
Poly
.
insertSorted
Nat
.
SOM
.
Poly
.
mulMon
Nat
.
SOM
.
Poly
.
mulMon
.
go
Nat
.
SOM
.
Poly
.
mul
Nat
.
SOM
.
Poly
.
mul
.
go
Nat
.
SOM
.
Expr
.
toPoly
Nat
.
SOM
.
Mon
.
append_denote
Nat
.
SOM
.
Mon
.
mul_denote
Nat
.
SOM
.
Mon
.
mul_denote
.
go
Nat
.
SOM
.
Poly
.
append_denote
Nat
.
SOM
.
Poly
.
add_denote
Nat
.
SOM
.
Poly
.
add_denote
.
go
Nat
.
SOM
.
Poly
.
denote_insertSorted
Nat
.
SOM
.
Poly
.
mulMon_denote
Nat
.
SOM
.
Poly
.
mulMon_denote
.
go
Nat
.
SOM
.
Poly
.
mul_denote
Nat
.
SOM
.
Poly
.
mul_denote
.
go
Nat
.
SOM
.
Expr
.
toPoly_denote
Nat
.
SOM
.
Expr
.
eq_of_toPoly_eq
source
inductive
Nat
.
SOM
.
Expr
:
Type
num
(
i
:
Nat
)
:
Expr
var
(
v
:
Linear.Var
)
:
Expr
add
(
a
b
:
Expr
)
:
Expr
mul
(
a
b
:
Expr
)
:
Expr
Instances For
source
instance
Nat
.
SOM
.
instInhabitedExpr
:
Inhabited
Expr
Equations
source
def
Nat
.
SOM
.
Expr
.
denote
(
ctx
:
Linear.Context
)
:
Expr
→
Nat
Equations
Instances For
source
@[reducible, inline]
abbrev
Nat
.
SOM
.
Mon
:
Type
Equations
Instances For
source
def
Nat
.
SOM
.
Mon
.
denote
(
ctx
:
Linear.Context
)
:
Mon
→
Nat
Equations
Instances For
source
def
Nat
.
SOM
.
Mon
.
mul
(
m₁
m₂
:
Mon
)
:
Mon
Equations
Instances For
source
def
Nat
.
SOM
.
Mon
.
mul
.
go
(
fuel
:
Nat
)
(
m₁
m₂
:
Mon
)
:
Mon
Equations
Instances For
source
@[reducible, inline]
abbrev
Nat
.
SOM
.
Poly
:
Type
Equations
Instances For
source
def
Nat
.
SOM
.
Poly
.
denote
(
ctx
:
Linear.Context
)
:
Poly
→
Nat
Equations
Instances For
source
def
Nat
.
SOM
.
Poly
.
add
(
p₁
p₂
:
Poly
)
:
Poly
Equations
Instances For
source
def
Nat
.
SOM
.
Poly
.
add
.
go
(
fuel
:
Nat
)
(
p₁
p₂
:
Poly
)
:
Poly
Equations
Instances For
source
def
Nat
.
SOM
.
Poly
.
insertSorted
(
k
:
Nat
)
(
m
:
Mon
)
(
p
:
Poly
)
:
Poly
Equations
Instances For
source
def
Nat
.
SOM
.
Poly
.
mulMon
(
p
:
Poly
)
(
k
:
Nat
)
(
m
:
Mon
)
:
Poly
Equations
Instances For
source
def
Nat
.
SOM
.
Poly
.
mulMon
.
go
(
k
:
Nat
)
(
m
:
Mon
)
(
p
acc
:
Poly
)
:
Poly
Equations
Instances For
source
def
Nat
.
SOM
.
Poly
.
mul
(
p₁
p₂
:
Poly
)
:
Poly
Equations
Instances For
source
def
Nat
.
SOM
.
Poly
.
mul
.
go
(
p₂
p₁
acc
:
Poly
)
:
Poly
Equations
Instances For
source
def
Nat
.
SOM
.
Expr
.
toPoly
:
Expr
→
Poly
Equations
Instances For
source
theorem
Nat
.
SOM
.
Mon
.
append_denote
(
ctx
:
Linear.Context
)
(
m₁
m₂
:
Mon
)
:
denote
ctx
(
m₁
++
m₂
)
=
denote
ctx
m₁
*
denote
ctx
m₂
source
theorem
Nat
.
SOM
.
Mon
.
mul_denote
(
ctx
:
Linear.Context
)
(
m₁
m₂
:
Mon
)
:
denote
ctx
(
m₁
.
mul
m₂
)
=
denote
ctx
m₁
*
denote
ctx
m₂
source
theorem
Nat
.
SOM
.
Mon
.
mul_denote
.
go
(
ctx
:
Linear.Context
)
(
fuel
:
Nat
)
(
m₁
m₂
:
Mon
)
:
denote
ctx
(
mul.go
fuel
m₁
m₂
)
=
denote
ctx
m₁
*
denote
ctx
m₂
source
theorem
Nat
.
SOM
.
Poly
.
append_denote
(
ctx
:
Linear.Context
)
(
p₁
p₂
:
Poly
)
:
denote
ctx
(
p₁
++
p₂
)
=
denote
ctx
p₁
+
denote
ctx
p₂
source
theorem
Nat
.
SOM
.
Poly
.
add_denote
(
ctx
:
Linear.Context
)
(
p₁
p₂
:
Poly
)
:
denote
ctx
(
p₁
.
add
p₂
)
=
denote
ctx
p₁
+
denote
ctx
p₂
source
theorem
Nat
.
SOM
.
Poly
.
add_denote
.
go
(
ctx
:
Linear.Context
)
(
fuel
:
Nat
)
(
p₁
p₂
:
Poly
)
:
denote
ctx
(
add.go
fuel
p₁
p₂
)
=
denote
ctx
p₁
+
denote
ctx
p₂
source
theorem
Nat
.
SOM
.
Poly
.
denote_insertSorted
(
ctx
:
Linear.Context
)
(
k
:
Nat
)
(
m
:
Mon
)
(
p
:
Poly
)
:
denote
ctx
(
insertSorted
k
m
p
)
=
denote
ctx
p
+
k
*
Mon.denote
ctx
m
source
theorem
Nat
.
SOM
.
Poly
.
mulMon_denote
(
ctx
:
Linear.Context
)
(
p
:
Poly
)
(
k
:
Nat
)
(
m
:
Mon
)
:
denote
ctx
(
p
.
mulMon
k
m
)
=
denote
ctx
p
*
k
*
Mon.denote
ctx
m
source
theorem
Nat
.
SOM
.
Poly
.
mulMon_denote
.
go
(
ctx
:
Linear.Context
)
(
k
:
Nat
)
(
m
:
Mon
)
(
p
acc
:
Poly
)
:
denote
ctx
(
mulMon.go
k
m
p
acc
)
=
denote
ctx
acc
+
denote
ctx
p
*
k
*
Mon.denote
ctx
m
source
theorem
Nat
.
SOM
.
Poly
.
mul_denote
(
ctx
:
Linear.Context
)
(
p₁
p₂
:
Poly
)
:
denote
ctx
(
p₁
.
mul
p₂
)
=
denote
ctx
p₁
*
denote
ctx
p₂
source
theorem
Nat
.
SOM
.
Poly
.
mul_denote
.
go
(
ctx
:
Linear.Context
)
(
p₂
p₁
acc
:
Poly
)
:
denote
ctx
(
mul.go
p₂
p₁
acc
)
=
denote
ctx
acc
+
denote
ctx
p₁
*
denote
ctx
p₂
source
theorem
Nat
.
SOM
.
Expr
.
toPoly_denote
(
ctx
:
Linear.Context
)
(
e
:
Expr
)
:
Poly.denote
ctx
e
.
toPoly
=
denote
ctx
e
source
theorem
Nat
.
SOM
.
Expr
.
eq_of_toPoly_eq
(
ctx
:
Linear.Context
)
(
a
b
:
Expr
)
(
h
: (
a
.
toPoly
==
b
.
toPoly
)
=
true
)
:
denote
ctx
a
=
denote
ctx
b