unfold function head
Equations
- One or more equations did not get rendered due to their size.
Instances For
Unfold function body head recursors and matches
Equations
- One or more equations did not get rendered due to their size.
Instances For
Synthesize instance of type type
and
- assign it to
x
ifx
is meta variable - check it is equal to
x
Equations
- One or more equations did not get rendered due to their size.
Instances For
Synthesize arguments xs
either with typeclass synthesis, with funProp or with discharger.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Try to apply theorem - core function
Equations
- One or more equations did not get rendered due to their size.
Instances For
Try to apply declared theorem
Equations
- One or more equations did not get rendered due to their size.
Instances For
Try to apply local theorem
Equations
- One or more equations did not get rendered due to their size.
Instances For
Apply lambda calculus rule P fun x => x`
Equations
- One or more equations did not get rendered due to their size.
Instances For
Apply lambda calculus rule P fun x => y`
Equations
- One or more equations did not get rendered due to their size.
Instances For
Apply lambda calculus rule P fun f => f i`
Equations
- One or more equations did not get rendered due to their size.
Instances For
Apply lambda calculus rule P f → P g → P fun x => f (g x)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Apply lambda calculus rule ∀ y, P (f · y) → P fun x y => f x y
Equations
- One or more equations did not get rendered due to their size.
Instances For
Changes the goal from P fun x => f x₁ x₂ x₃
to P fun x => f x₁ x₂
TODO: be able to provide number of arguments
Equations
- One or more equations did not get rendered due to their size.
Instances For
Determina if e
is talking about a free variable and about which arguments.
For example:
- for
Continuous f
this function returns fvar id off
and#[0]
- for
Continuous fun x => f x y
this function returns fvar id off
and#[1]
- for
Continuous fun (x,y) => f x y
this function returns fvar id off
and#[0,1]
- for
Continuous fun xy => f xy.1 xy.2
this function returns fvar id off
and#[0,1]
This function is assuming:
- that
e
is talking about function propertyfunPropDecl
- the function
f
ine
can't be expressed as composition of two non-trivial functions this means thatf == (← splitLambdaToComp f).1
is true
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prove function property of free variable by using local hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prove function property of using local hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prove function property of fun x => let y := g x; f x y
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prove function property of fun f => f x₁ ... xₙ
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prove function property of using "morphism theorems" e.g. bundled linear map is linear map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prove function property of using "transition theorems" e.g. continuity from linearity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prove function property of fun x => f x₁ ... xₙ
where f
is declared function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prove function property of fun x => f x₁ ... xₙ
where f
is free variable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cache result if it does not have any subgoals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Main funProp
function. Returns proof of e
.