In addition to the tactics found in the core library, mathlib provides a number of specific interactive tactics. Here we document the mostly commonly used ones, as well as some underdocumented tactics from core.
Evaluate expressions in the language of additive, commutative monoids and groups.
It attempts to prove the goal outright if there is no at
specifier and the target is an equality, but if this
fails, it falls back to rewriting all monoid expressions into a normal form.
If there is an at
specifier, it rewrites the given target into a normal form.
example {α : Type*} {a b : α} [add_comm_monoid α] : a + (b + a) = a + a + b := by abel
example {α : Type*} {a b : α} [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel
example {α : Type*} {a b : α} [add_comm_group α] (hyp : a + a - a = b - b) : a = 0 :=
by { abel at hyp, exact hyp }
ac_mono
reduces the f x ⊑ f y
, for some relation ⊑
and a
monotonic function f
to x ≺ y
.
ac_mono*
unwraps monotonic functions until it can't.
ac_mono^k
, for some literal number k
applies monotonicity k
times.
ac_mono h
, with h
a hypothesis, unwraps monotonic functions and
uses h
to solve the remaining goal. Can be combined with *
or ^k
:
ac_mono* h
ac_mono : p
asserts p
and uses it to discharge the goal result
unwrapping a series of monotonic functions. Can be combined with * or
^k: ac_mono* : p
In the case where f
is an associative or commutative operator,
ac_mono
will consider any possible permutation of its arguments and
use the one the minimizes the difference between the left-hand side
and the right-hand side.
To use it, first import tactic.monotonicity
.
ac_mono
can be used as follows:
example (x y z k m n : ℕ)
(h₀ : z ≥ 0)
(h₁ : x ≤ y) :
(m + x + n) * z + k ≤ z * (y + n + m) + k :=
begin
ac_mono,
-- ⊢ (m + x + n) * z ≤ z * (y + n + m)
ac_mono,
-- ⊢ m + x + n ≤ y + n + m
ac_mono,
end
As with mono*
, ac_mono*
solves the goal in one go and so does
ac_mono* h₁
. The latter syntax becomes especially interesting in the
following example:
example (x y z k m n : ℕ)
(h₀ : z ≥ 0)
(h₁ : m + x + n ≤ y + n + m) :
(m + x + n) * z + k ≤ z * (y + n + m) + k :=
by ac_mono* h₁.
By giving ac_mono
the assumption h₁
, we are asking ac_refl
to
stop earlier than it would normally would.
Apply a function to some local assumptions which are either equalities
or inequalities. For instance, if the context contains h : a = b
and
some function f
then apply_fun f at h
turns h
into
h : f a = f b
. When the assumption is an inequality h : a ≤ b
, a side
goal monotone f
is created, unless this condition is provided using
apply_fun f at h using P
where P : monotone f
, or the mono
tactic
can prove it.
Typical usage is:
open function
example (X Y Z : Type) (f : X → Y) (g : Y → Z) (H : injective $ g ∘ f) :
injective f :=
begin
intros x x' h,
apply_fun g at h,
exact H h
end
apply_rules hs n
applies the list of lemmas hs
and assumption
on the
first goal and the resulting subgoals, iteratively, at most n
times.
n
is optional, equal to 50 by default.
hs
can contain user attributes: in this case all theorems with this
attribute are added to the list of rules.
For instance:
@[user_attribute]
meta def mono_rules : user_attribute :=
{ name := `mono_rules,
descr := "lemmas usable to prove monotonicity" }
attribute [mono_rules] add_le_add mul_le_mul_of_nonneg_right
lemma my_test {a b c d e : real} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 0 ≤ e) :
a + c * e + a + c + 0 ≤ b + d * e + b + d + e :=
-- any of the following lines solve the goal:
add_le_add (add_le_add (add_le_add (add_le_add h1 (mul_le_mul_of_nonneg_right h2 h3)) h1 ) h2) h3
by apply_rules [add_le_add, mul_le_mul_of_nonneg_right]
by apply_rules [mono_rules]
by apply_rules mono_rules
assoc_rewrite [h₀, ← h₁] at ⊢ h₂
behaves like
rewrite [h₀, ← h₁] at ⊢ h₂
with the exception that associativity is
used implicitly to make rewriting possible.
The congruence closure tactic cc
tries to solve the goal by chaining
equalities from context and applying congruence (ie if a = b
then f a = f b
).
It is a finishing tactic, ie is meant to close
the current goal, not to make some inconclusive progress.
A mostly trivial example would be:
example (a b c : ℕ) (f : ℕ → ℕ) (h: a = b) (h' : b = c) : f a = f c := by cc
As an example requiring some thinking to do by hand, consider:
example (f : ℕ → ℕ) (x : ℕ)
(H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) :
f x = x :=
by cc
The tactic works by building an equality matching graph. It's a graph where the vertices are terms and they are linked by edges if they are known to be equal. Once you've added all the equalities in your context, you take the transitive closure of the graph and, for each connected component (i.e. equivalence class) you can elect a term that will represent the whole class and store proofs that the other elements are equal to it. You then take the transitive closure of these equalities under the congruence lemmas.
The cc
implementation in Lean does a few more tricks: for example it
derives a=b
from nat.succ a = nat.succ b
, and nat.succ a !=
nat.zero
for any a
.
The starting reference point is Nelson, Oppen, Fast decision procedures based on congruence closure, Journal of the ACM (1980)
The congruence lemmas for dependent type theory as used in Lean are described in Congruence closure in intensional type theory (de Moura, Selsam IJCAR 2016).
choose a b h using hyp
takes an hypothesis hyp
of the form
∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b
for some P : X → Y → A → B → Prop
and outputs
into context a function a : X → Y → A
, b : X → Y → B
and a proposition h
stating
∀ (x : X) (y : Y), P x y (a x y) (b x y)
. It presumably also works with dependent versions.
Example:
example (h : ∀n m : ℕ, ∃i j, m = n + i ∨ m + j = n) : true :=
begin
choose i j h using h,
guard_hyp i := ℕ → ℕ → ℕ,
guard_hyp j := ℕ → ℕ → ℕ,
guard_hyp h := ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n,
trivial
end
clear_aux_decl
clears every aux_decl
in the local context for the current goal.
This includes the induction hypothesis when using the equation compiler and
_let_match
and _fun_match
.
It is useful when using a tactic such as finish
, simp *
or subst
that may use these
auxiliary declarations, and produce an error saying the recursion is not well founded.
example (n m : ℕ) (h₁ : n = m) (h₂ : ∃ a : ℕ, a = n ∧ a = m) : 2 * m = 2 * n :=
let ⟨a, ha⟩ := h₂ in
begin
clear_aux_decl, -- subst will fail without this line
subst h₁
end
example (x y : ℕ) (h₁ : ∃ n : ℕ, n * 1 = 2) (h₂ : 1 + 1 = 2 → x * 1 = y) : x = y :=
let ⟨n, hn⟩ := h₁ in
begin
clear_aux_decl, -- finish produces an error without this line
finish
end
Same as the congr
tactic, but takes an optional argument which gives
the depth of recursive applications. This is useful when congr
is too aggressive in breaking down the goal. For example, given
⊢ f (g (x + y)) = f (g (y + x))
, congr'
produces the goals ⊢ x = y
and ⊢ y = x
, while congr' 2
produces the intended ⊢ x + y = y + x
.
If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.
Transforms the goal into its contrapositive.
contrapose
turns a goal P → Q
into ¬ Q → ¬ P
contrapose!
turns a goal P → Q
into ¬ Q → ¬ P
and pushes negations inside P
and Q
using push_neg
contrapose h
first reverts the local assumption h
, and then uses contrapose
and intro h
contrapose! h
first reverts the local assumption h
, and then uses contrapose!
and intro h
contrapose h with new_h
uses the name new_h
for the introduced hypothesis
The conv
tactic is built-in to lean. Inside conv
blocks mathlib currently
additionally provides
erw
,ring
and ring2
,norm_num
, andconv
(within another conv
).
Using conv
inside a conv
block allows the user to return to the previous
state of the outer conv
block after it is finished. Thus you can continue
editing an expression without having to start a new conv
block and re-scoping
everything. For example:example (a b c d : ℕ) (h₁ : b = c) (h₂ : a + c = a + d) : a + b = a + d :=
by conv {
to_lhs,
conv {
congr, skip,
rw h₁,
},
rw h₂,
}
Without conv
the above example would need to be proved using two successive
conv
blocks each beginning with to_lhs
.
Also, as a shorthand conv_lhs
and conv_rhs
are provided, so that
example : 0 + 0 = 0 :=
begin
conv_lhs { simp }
end
just means
example : 0 + 0 = 0 :=
begin
conv { to_lhs, simp }
end
and likewise for to_rhs
.
The exact e
and refine e
tactics require a term e
whose type is
definitionally equal to the goal. convert e
is similar to refine
e
, but the type of e
is not required to exactly match the
goal. Instead, new goals are created for differences between the type
of e
and the goal. For example, in the proof state
n : ℕ,
e : prime (2 * n + 1)
⊢ prime (n + n + 1)
the tactic convert e
will change the goal to
⊢ n + n = 2 * n
In this example, the new goal can be solved using ring
.
The syntax convert ← e
will reverse the direction of the new goals
(producing ⊢ 2 * n = n + n
in this example).
Internally, convert e
works by creating a new goal asserting that
the goal equals the type of e
, then simplifying it using
congr'
. The syntax convert e using n
can be used to control the
depth of matching (like congr' n
). In the example, convert e using
1
would produce a new goal ⊢ n + n + 1 = 2 * n + 1
.
convert_to g using n
attempts to change the current goal to g
, but unlike change
,
it will generate equality proof obligations using congr' n
to resolve discrepancies.
convert_to g
defaults to using congr' 1
.
ac_change
is convert_to
followed by ac_refl
. It is useful for rearranging/reassociating
e.g. sums:
example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N :=
begin
ac_change a + d + e + f + c + g + b ≤ _,
-- ⊢ a + d + e + f + c + g + b ≤ N
end
def_replacer foo
sets up a stub definition foo : tactic unit
, which can
effectively be defined and re-defined later, by tagging definitions with @[foo]
.
@[foo] meta def foo_1 : tactic unit := ...
replaces the current definition of foo
.@[foo] meta def foo_2 (old : tactic unit) : tactic unit := ...
replaces the current
definition of foo
, and provides access to the previous definition via old
.
(The argument can also be an option (tactic unit)
, which is provided as none
if
this is the first definition tagged with @[foo]
since def_replacer
was invoked.)def_replacer foo : α → β → tactic γ
allows the specification of a replacer with
custom input and output types. In this case all subsequent redefinitions must have the
same type, or the type α → β → tactic γ → tactic γ
or
α → β → option (tactic γ) → tactic γ
analogously to the previous cases.
default_dec_tac'
is a replacement for the core tactic default_dec_tac
, fixing a bug. This
bug is often indicated by a message nested exception message: tactic failed, there are no goals to be solved
,and solved by appending using_well_founded wf_tacs
to the recursive definition.
See also additional documentation of using_well_founded
in
docs/extras/well_founded_recursion.md.
The elide n (at ...)
tactic hides all subterms of the target goal or hypotheses
beyond depth n
by replacing them with hidden
, which is a variant
on the identity function. (Tactics should still mostly be able to see
through the abbreviation, but if you want to unhide the term you can use
unelide
.)
The unelide (at ...)
tactic removes all hidden
subterms in the target
types (usually added by elide
).
ext1 id
selects and apply one extensionality lemma (with
attribute ext
), using id
, if provided, to name a
local constant introduced by the lemma. If id
is omitted, the
local constant is named automatically, as per intro
.
ext
applies as many extensionality lemmas as possible;
ext ids
, with ids
a list of identifiers, finds extentionality
and applies them until it runs out of identifiers in ids
to name
the local constants.When trying to prove:
lean
α β : Type,
f g : α → set β
⊢ f = g
applying ext x y
yields:
lean
α β : Type,
f g : α → set β,
x : α,
y : β
⊢ y ∈ f x ↔ y ∈ g x
by applying functional extensionality and set extensionality.
A maximum depth can be provided with ext x y z : 3
.
The goal of field_simp
is to reduce an expression in a field to an expression of the form n / d
where neither n
nor d
contains any division symbol, just using the simplifier (with a carefully
crafted simpset named field_simps
) to reduce the number of division symbols whenever possible by
iterating the following steps:
If the goal is an equality, this simpset will also clear the denominators, so that the proof
can normally be concluded by an application of ring
or ring_exp
.
field_simp [hx, hy]
is a short form for simp [-one_div_eq_inv, hx, hy] with field_simps
Note that this naive algorithm will not try to detect common factors in denominators to reduce the
complexity of the resulting expression. Instead, it relies on the ability of ring
to handle
complicated expressions in the next step.
As always with the simplifier, reduction steps will only be applied if the preconditions of the lemmas can be checked. This means that proofs that denominators are nonzero should be included. The fact that a product is nonzero when all factors are, and that a power of a nonzero number is nonzero, are included in the simpset, but more complicated assertions (especially dealing with sums) should be given explicitly. If your expression is not completely reduced by the simplifier invocation, check the denominators of the resulting expression and provide proofs that they are nonzero to enable further progress.
The invocation of field_simp
removes the lemma one_div_eq_inv
(which is marked as a simp lemma
in core) from the simpset, as this lemma works against the algorithm explained above.
For example,
example (a b c d x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0) :
a + b / x + c / x^2 + d / x^3 = a + x⁻¹ * (y * b / y + (d / x + c) / x) :=
begin
field_simp [hx, hy],
ring
end
fin_cases h
performs case analysis on a hypothesis of the form
1) h : A
, where [fintype A]
is available, or
2) h ∈ A
, where A : finset X
, A : multiset X
or A : list X
.
fin_cases *
performs case analysis on all suitable hypotheses.
As an example, in
example (f : ℕ → Prop) (p : fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val :=
begin
fin_cases p; simp,
all_goals { assumption }
end
after fin_cases p; simp
, there are three goals, f 0
, f 1
, and f 2
.
These tactics do straightforward things: they call the simplifier, split conjunctive assumptions, eliminate existential quantifiers on the left, and look for contradictions. They rely on ematching and congruence closure to try to finish off a goal at the end.
The procedures do split on disjunctions and recreate the smt state for each terminal call, so they are only meant to be used on small, straightforward problems.
All accept an optional list of simplifier rules, typically definitions that should be expanded.
(The equations and identities should not refer to the local context.) All also accept an optional list of ematch
lemmas, which must be preceded by using
.
h_generalize Hx : e == x
matches on cast _ e
in the goal and replaces it with
x
. It also adds Hx : e == x
as an assumption. If cast _ e
appears multiple
times (not necessarily with the same proof), they are all replaced by x
. cast
eq.mp
, eq.mpr
, eq.subst
, eq.substr
, eq.rec
and eq.rec_on
are all treated
as casts.
h_generalize Hx : e == x with h
adds hypothesis α = β
with e : α, x : β
;h_generalize Hx : e == x with _
chooses automatically chooses the name of
assumption α = β
;
h_generalize! Hx : e == x
reverts Hx
;Hx
is omitted, assumption Hx : e == x
is not added.import_private foo from bar
finds a private declaration foo
in the same file as bar
and creates a
local notation to refer to it.
import_private foo
, looks for foo
in all (imported) files.
When possible, make foo
non-private rather than using this feature.
For performance reasons, Lean does not automatically update its database
of class instances during a proof. The group of tactics described below
helps forcing such updates. For a simple (but very artificial) example,
consider the function default
from the core library. It has type
Π (α : Sort u) [inhabited α], α
, so one can use default α
only if Lean
can find a registered instance of inhabited α
. Because the database of
such instance is not automatically updated during a proof, the following
attempt won't work (Lean will not pick up the instance from the local
context):
def my_id (α : Type) : α → α :=
begin
intro x,
have : inhabited α := ⟨x⟩,
exact default α, -- Won't work!
end
However, it will work, producing the identity function, if one replaces have by its variant haveI
described below.
resetI
: Reset the instance cache. This allows any instances
currently in the context to be used in typeclass inference.
unfreezeI
: Unfreeze local instances, which allows us to revert
instances in the context
introI
/introsI
: intro
/intros
followed by resetI
. Like
intro
/intros
, but uses the introduced variable in typeclass inference.
haveI
/letI
: have
/let
followed by resetI
. Used to add typeclasses
to the context so that they can be used in typeclass inference. The syntax
haveI := <proof>
and haveI : t := <proof>
is supported, but
haveI : t, from _
and haveI : t, { <proof> }
are not; in these cases
use have : t, { <proof> }, resetI
directly).
exactI
: resetI
followed by exact
. Like exact
, but uses all
variables in the context for typeclass inference.
library_search
is a tactic to identify existing lemmas in the library. It tries to close the
current goal by applying a lemma from the library, then discharging any new goals using
solve_by_elim
.
Typical usage is:
example (n m k : ℕ) : n * (m - k) = n * m - n * k :=
by library_search -- exact nat.mul_sub_left_distrib n m k
library_search
prints a trace message showing the proof it found, shown above as a comment.
Typically you will then copy and paste this proof, replacing the call to library_search
.
Lift an expression to another type.
'lift' expr 'to' expr ('using' expr)? ('with' id (id id?)?)?
.n : ℤ
and hn : n ≥ 0
then the tactic lift n to ℕ using hn
creates a new
constant of type ℕ
, also named n
and replaces all occurrences of the old variable (n : ℤ)
with ↑n
(where n
in the new variable). It will remove n
and hn
from the context.
lift n to ℕ using hn
transforms the goal
n : ℤ, hn : n ≥ 0, h : P n ⊢ n = 3
to n : ℕ, h : P ↑n ⊢ ↑n = 3
(here P
is some term of type ℤ → Prop
).using hn
is optional, the tactic lift n to ℕ
does the same, but also creates a
new subgoal that n ≥ 0
(where n
is the old variable).
lift n to ℕ
transforms the goal
n : ℤ, h : P n ⊢ n = 3
to two goals
n : ℕ, h : P ↑n ⊢ ↑n = 3
and n : ℤ, h : P n ⊢ n ≥ 0
.lift n to ℕ using e
where e
is any expression of type n ≥ 0
.lift n to ℕ with k
to specify the name of the new variable.lift n to ℕ with k hk
to also specify the name of the equality ↑k = n
. In this case, n
will remain in the context. You can use rfl
for the name of hk
to substitute n
away
(i.e. the default behavior).lift e to ℕ with k hk
where e
is any expression of type ℤ
.
In this case, the hk
will always stay in the context, but it will be used to rewrite e
in
all hypotheses and the target.
lift n + 3 to ℕ using hn with k hk
transforms the goal
n : ℤ, hn : n + 3 ≥ 0, h : P (n + 3) ⊢ n + 3 = 2 * n
to the goal
n : ℤ, k : ℕ, hk : ↑k = n + 3, h : P ↑k ⊢ ↑k = 2 * n
.lift n to ℕ using h
will remove h
from the context. If you want to keep it,
specify it again as the third argument to with
, like this: lift n to ℕ using h with n rfl h
.α
to β
assuming that there is an instance
of can_lift α β
. In this case the proof obligation is specified by can_lift.cond
.can_lift β γ
, it can also lift α → β
to α → γ
; more generally, given
β : Π a : α, Type*
, γ : Π a : α, Type*
, and [Π a : α, can_lift (β a) (γ a)]
, it automatically
generates an instance can_lift (Π a, β a) (Π a, γ a)
.linarith
attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving false
.
In theory, linarith
should prove any goal that is true in the theory of linear arithmetic over the rationals. While there is some special handling for non-dense orders like nat
and int
, this tactic is not complete for these theories and will not prove every true goal.
An example:
example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
(h3 : 12*y - 4* z < 0) : false :=
by linarith
linarith
will use all appropriate hypotheses and the negation of the goal, if applicable.
linarith [t1, t2, t3]
will additionally use proof terms t1, t2, t3
.
linarith only [h1, h2, h3, t1, t2, t3]
will use only the goal (if relevant), local hypotheses
h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context.
linarith!
will use a stronger reducibility setting to try to identify atoms. For example,
example (x : ℚ) : id x ≥ x :=
by linarith
will fail, because linarith
will not identify x
and id x
. linarith!
will.
This can sometimes be expensive.
linarith {discharger := tac, restrict_type := tp, exfalso := ff}
takes a config object with three optional
arguments.
discharger
specifies a tactic to be used for reducing an algebraic equation in the
proof stage. The default is ring
. Other options currently include ring SOP
or simp
for basic
problems.restrict_type
will only use hypotheses that are inequalities over tp
. This is useful
if you have e.g. both integer and rational valued inequalities in the local context, which can
sometimes confuse the tactic.exfalso
is false, linarith
will fail when the goal is neither an inequality nor false
. (True by default.)mono
applies a monotonicity rule.mono*
applies monotonicity rules repetitively.mono with x ≤ y
or mono with [0 ≤ x,0 ≤ y]
creates an assertion for the listed
propositions. Those help to select the right monotonicity rule.mono left
or mono right
is useful when proving strict orderings:
for x + y < w + z
could be broken down into either
x ≤ w
and y < z
orx < w
and y ≤ z
To use it, first import tactic.monotonicity
.
Here is an example of mono:
example (x y z k : ℤ)
(h : 3 ≤ (4 : ℤ))
(h' : z ≤ y) :
(k + 3 + x) - y ≤ (k + 4 + x) - z :=
begin
mono, -- unfold `(-)`, apply add_le_add
{ -- ⊢ k + 3 + x ≤ k + 4 + x
mono, -- apply add_le_add, refl
-- ⊢ k + 3 ≤ k + 4
mono },
{ -- ⊢ -y ≤ -z
mono /- apply neg_le_neg -/ }
end
More succinctly, we can prove the same goal as:
example (x y z k : ℤ)
(h : 3 ≤ (4 : ℤ))
(h' : z ≤ y) :
(k + 3 + x) - y ≤ (k + 4 + x) - z :=
by mono*
This tactic normalizes casts inside expressions. It is basically a simp tactic with a specific set of lemmas to move casts upwards in the expression. Therefore it can be used more safely as a non-terminating tactic. It also has special handling of numerals.
For instance, given an assumption
a b : ℤ
h : ↑a + ↑b < (10 : ℚ)
writing norm_cast at h
will turn h
into
h : a + b < 10
You can also use exact_mod_cast
, apply_mod_cast
, rw_mod_cast
or assumption_mod_cast
.
Writing exact_mod_cast h
and apply_mod_cast h
will normalize the goal and h before using exact h
or apply h
.
Writing assumption_mod_cast
will normalize the goal and for every
expression h
in the context it will try to normalize h
and use
exact h
.
rw_mod_cast
acts like the rw
tactic but it applies norm_cast
between steps.
These tactics work with three attributes,
elim_cast
, move_cast
and squash_cast
.
elim_cast
is for elimination lemmas of the shape
Π ..., P ↑a1 ... ↑an = P a1 ... an
, for instance:
int.coe_nat_inj' : ∀ {m n : ℕ}, ↑m = ↑n ↔ m = n
rat.coe_int_denom : ∀ (n : ℤ), ↑n.denom = 1
move_cast
is for compositional lemmas of the shape
Π ..., ↑(P a1 ... an) = P ↑a1 ... ↑an
, for instance:
int.coe_nat_add : ∀ (m n : ℕ), ↑(m + n) = ↑m + ↑n`
nat.cast_sub : ∀ {α : Type*} [add_group α] [has_one α] {m n : ℕ}, m ≤ n → ↑(n - m) = ↑n - ↑m
squash_cast
is for lemmas of the shape
Π ..., ↑↑a = ↑a
, for instance:
int.cast_coe_nat : ∀ (n : ℕ), ↑↑n = ↑n
int.cats_id : int.cast_id : ∀ (n : ℤ), ↑n = n
push_cast
rewrites the expression to move casts toward the leaf nodes.
This uses move_cast
lemmas in the "forward" direction.
For example, ↑(a + b)
will be written to ↑a + ↑b
.
It is equivalent to simp only with push_cast
, and can also be used at hypotheses
with push_cast at h
.
Normalises numerical expressions. It supports the operations +
-
*
/
^
and %
over numerical types such as ℕ
, ℤ
, ℚ
, ℝ
, ℂ
, and can prove goals of the form A = B
, A ≠ B
, A < B
and A ≤ B
, where A
and B
are
numerical expressions. It also has a relatively simple primality prover.
import data.real.basic
example : (2 : ℝ) + 2 = 4 := by norm_num
example : (12345.2 : ℝ) ≠ 12345.3 := by norm_num
example : (73 : ℝ) < 789/2 := by norm_num
example : 123456789 + 987654321 =<PHONE_NUMBER> := by norm_num
example (R : Type*) [ring R] : (2 : R) + 2 = 4 := by norm_num
example (F : Type*) [linear_ordered_field F] : (2 : F) + 2 < 5 := by norm_num
example : nat.prime (2^13 - 1) := by norm_num
example : ¬ nat.prime (2^11 - 1) := by norm_num
example (x : ℝ) (h : x = 123 + 456) : x = 579 := by norm_num at h; assumption
The obtain
tactic is a combination of have
and rcases
.
obtain ⟨patt⟩ : type,
{ ... }
is equivalent to
have h : type,
{ ... },
rcases h with ⟨patt⟩
The syntax obtain ⟨patt⟩ : type := proof
is also supported.
If ⟨patt⟩
is omitted, rcases
will try to infer the pattern.
If type
is omitted, := proof
is required.
omega
attempts to discharge goals in the quantifier-free fragment of linear integer and natural number arithmetic using the Omega test. In other words, the core procedure of omega
works with goals of the form
∀ x₁, ... ∀ xₖ, P
where x₁, ... xₖ
are integer (resp. natural number) variables, and P
is a quantifier-free formula of linear integer (resp. natural number) arithmetic. For instance:
example : ∀ (x y : int), (x ≤ 5 ∧ y ≤ 3) → x + y ≤ 8 := by omega
By default, omega
tries to guess the correct domain by looking at the goal and hypotheses, and then reverts all relevant hypotheses and variables (e.g., all variables of type nat
and Prop
s in linear natural number arithmetic, if the domain was determined to be nat
) to universally close the goal before calling the main procedure. Therefore, omega
will often work even if the goal is not in the above form:
example (x y : nat) (h : 2 * x + 1 = 2 * y) : false := by omega
But this behaviour is not always optimal, since it may revert irrelevant hypotheses or incorrectly guess the domain. Use omega manual
to disable automatic reverts, and omega int
or omega nat
to specify the domain.
example (x y z w : int) (h1 : 3 * y ≥ x) (h2 : z > 19 * w) : 3 * x ≤ 9 * y :=
by {revert h1 x y, omega manual}
example (i : int) (n : nat) (h1 : i = 0) (h2 : n < n) : false := by omega nat
example (n : nat) (h1 : n < 34) (i : int) (h2 : i * 9 = -72) : i = -8 :=
by {revert h2 i, omega manual int}
omega
handles nat
subtraction by repeatedly rewriting goals of the form P[t-s]
into P[x] ∧ (t = s + x ∨ (t ≤ s ∧ x = 0))
, where x
is fresh. This means that each (distinct) occurrence of subtraction will cause the goal size to double during DNF transformation.
omega
implements the real shadow step of the Omega test, but not the dark and gray shadows. Therefore, it should (in principle) succeed whenever the negation of the goal has no real solution, but it may fail if a real solution exists, even if there is no integer/natural number solution.
pi_instance
constructs an instance of my_class (Π i : I, f i)
where we know Π i, my_class (f i)
. If an order relation is required,
it defaults to pi.partial_order
. Any field of the instance that
pi_instance
cannot construct is left untouched and generated as a
new goal.
This tactic pushes negations inside expressions. For instance, given an assumption
h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)
writing push_neg at h
will turn h
into
h : ∃ ε, ε > 0 ∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
(the pretty printer does not use the abreviations ∀ δ > 0
and ∃ ε > 0
but this issue
has nothing to do with push_neg
).
Note that names are conserved by this tactic, contrary to what would happen with simp
using the relevant lemmas. One can also use this tactic at the goal using push_neg
,
at every assumption and the goal using push_neg at *
or at selected assumptions and the goal
using say push_neg at h h' ⊢
as usual.
The rcases
tactic is the same as cases
, but with more flexibility in the
with
pattern syntax to allow for recursive case splitting. The pattern syntax
uses the following recursive grammar:
patt ::= (patt_list "|")* patt_list
patt_list ::= id | "_" | "⟨" (patt ",")* patt "⟩"
A pattern like ⟨a, b, c⟩ | ⟨d, e⟩
will do a split over the inductive
datatype, naming the first three parameters of the first constructor as
a,b,c
and the first two of the second constructor d,e
. If the list
is not as long as the number of arguments to the constructor or the
number of constructors, the remaining variables will be automatically
named. If there are nested brackets such as ⟨⟨a⟩, b | c⟩ | d
then
these will cause more case splits as necessary. If there are too many
arguments, such as ⟨a, b, c⟩
for splitting on ∃ x, ∃ y, p x
, then it
will be treated as ⟨a, ⟨b, c⟩⟩
, splitting the last parameter as
necessary.
rcases
also has special support for quotient types: quotient induction into Prop works like
matching on the constructor quot.mk
.
rcases h : e with PAT
will do the same as rcases e with PAT
with the exception that an assumption
h : e = PAT
will be added to the context.
rcases? e
will perform case splits on e
in the same way as rcases e
,
but rather than accepting a pattern, it does a maximal cases and prints the
pattern that would produce this case splitting. The default maximum depth is 5,
but this can be modified with rcases? e : n
.
refine_struct { .. }
acts like refine
but works only with structure instance
literals. It creates a goal for each missing field and tags it with the name of the
field so that have_field
can be used to generically refer to the field currently
being refined.
As an example, we can use refine_struct
to automate the construction semigroup
instances:
refine_struct ( { .. } : semigroup α ),
-- case semigroup, mul
-- α : Type u,
-- ⊢ α → α → α
-- case semigroup, mul_assoc
-- α : Type u,
-- ⊢ ∀ (a b c : α), a * b * c = a * (b * c)
have_field
, used after refine_struct _
poses field
as a local constant
with the type of the field of the current goal:
refine_struct ({ .. } : semigroup α),
{ have_field, ... },
{ have_field, ... },
behaves like
refine_struct ({ .. } : semigroup α),
{ have field := @semigroup.mul, ... },
{ have field := @semigroup.mul_assoc, ... },
Acts like have
, but removes a hypothesis with the same name as
this one. For example if the state is h : p ⊢ goal
and f : p → q
,
then after replace h := f h
the goal will be h : q ⊢ goal
,
where have h := f h
would result in the state h : p, h : q ⊢ goal
.
This can be used to simulate the specialize
and apply at
tactics
of Coq.
restate_axiom
makes a new copy of a structure field, first definitionally simplifying the type.
This is useful to remove auto_param
or opt_param
from the statement.
As an example, we have:
structure A :=
(x : ℕ)
(a' : x = 1 . skip)
example (z : A) : z.x = 1 := by rw A.a' -- rewrite tactic failed, lemma is not an equality nor a iff
restate_axiom A.a'
example (z : A) : z.x = 1 := by rw A.a
By default, restate_axiom
names the new lemma by removing a trailing '
, or otherwise appending
_lemma
if there is no trailing '
. You can also give restate_axiom
a second argument to
specify the new name, as in
restate_axiom A.a f
example (z : A) : z.x = 1 := by rw A.f
Evaluate expressions in the language of commutative (semi)rings. Based on Proving Equalities in a Commutative Ring Done Right in Coq by Benjamin Grégoire and Assia Mahboubi.
The variant ring!
uses a more aggessive reducibility setting to determine equality of atoms.
Evaluate expressions in commutative (semi)rings, allowing for variables in the exponent.
This tactic extends ring
: it should solve every goal that ring
can solve.
Additionally, it knows how to evaluate expressions with complicated exponents
(where ring
only understands constant exponents).
The variants ring_exp!
and ring_exp_eq!
use a more aggessive reducibility setting to determine equality of atoms.
For example:
example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring_exp
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring_exp
example (x y : ℕ) : x + id y = y + id x := by ring_exp!
The rintro
tactic is a combination of the intros
tactic with rcases
to
allow for destructuring patterns while introducing variables. See rcases
for
a description of supported patterns. For example, rintros (a | ⟨b, c⟩) ⟨d, e⟩
will introduce two variables, and then do case splits on both of them producing
two subgoals, one with variables a d e
and the other with b c d e
.
rintro?
will introduce and case split on variables in the same way as
rintro
, but will also print the rintro
invocation that would have the same
result. Like rcases?
, rintro? : n
allows for modifying the
depth of splitting; the default is 5.
rotate
moves the first goal to the back. rotate n
will do this n
times.
set a := t with h
is a variant of let a := t
. It adds the hypothesis h : a = t
to the local context and replaces t
with a
everywhere it can.
set a := t with ←h
will add h : t = a
instead.
set! a := t with h
does not do any replacing.
example (x : ℕ) (h : x = 3) : x + x + x = 9 :=
begin
set y := x with ←h_xy,
/-
x : ℕ,
y : ℕ := x,
h_xy : x = y,
h : y = 3
⊢ y + y + y = 9
-/
end
This is a "finishing" tactic modification of simp
. It has two forms.
simpa [rules, ...] using e
will simplify the goal and the type of
e
using rules
, then try to close the goal using e
.
Simplifying the type of e
makes it more likely to match the goal
(which has also been simplified). This construction also tends to be
more robust under changes to the simp lemma set.
simpa [rules, ...]
will simplify the goal and the type of a
hypothesis this
if present in the context, then try to close the goal using
the assumption
tactic.
The tactic solve_by_elim
repeatedly applies assumptions to the current goal, and succeeds if this eventually discharges the main goal.
solve_by_elim { discharger := `[cc] }
also attempts to discharge the goal using congruence closure before each round of applying assumptions.
solve_by_elim*
tries to solve all goals together, using backtracking if a solution for one goal
makes other goals impossible.
By default solve_by_elim
also applies congr_fun
and congr_arg
against the goal.
The assumptions can be modified with similar syntax as for simp
:
solve_by_elim [h₁, h₂, ..., hᵣ]
also applies the named lemmas (or all lemmas tagged with the named
attributes).solve_by_elim only [h₁, h₂, ..., hᵣ]
does not include the local context, congr_fun
, or congr_arg
unless they are explicitly included.solve_by_elim [-id_1, ... -id_n]
uses the default assumptions, removing the specified ones.squeeze_simp
and squeeze_simpa
perform the same task with
the difference that squeeze_simp
relates to simp
while
squeeze_simpa
relates to simpa
. The following applies to both
squeeze_simp
and squeeze_simpa
.
squeeze_simp
behaves like simp
(including all its arguments)
and prints a simp only
invokation to skip the search through the
simp
lemma list.
For instance, the following is easily solved with simp
:
example : 0 + 1 = 1 + 0 := by simp
To guide the proof search and speed it up, we may replace simp
with squeeze_simp
:
example : 0 + 1 = 1 + 0 := by squeeze_simp
-- prints: simp only [add_zero, eq_self_iff_true, zero_add]
squeeze_simp
suggests a replacement which we can use instead of
squeeze_simp
.
example : 0 + 1 = 1 + 0 := by simp only [add_zero, eq_self_iff_true, zero_add]
squeeze_simp only
prints nothing as it already skips the simp
list.
This tactic is useful for speeding up the compilation of a complete file. Steps:
simp
with squeeze_simp
(the space helps avoid the
replacement of simp
in @[simp]
) throughout the file.squeeze_simp
.squeeze_simp
with
simp
to remove the occurrences of squeeze_simp
that did not produce a suggestion.Known limitation(s):
squeeze_simp
is used after a ;
(e.g. cases x; squeeze_simp
),
squeeze_simp
will produce as many suggestions as the number of goals it is applied to.
It is likely that none of the suggestion is a good replacement but they can all be
combined by concatenating their list of lemmas.suggest
lists possible usages of the refine
tactic and leaves the tactic state unchanged.
It is intended as a complement of the search function in your editor, the #find
tactic, and library_search
.
suggest
takes an optional natural number num
as input and returns the first num
(or less, if all possibilities are exhausted) possibilities ordered by length of lemma names. The default for num
is 50
.
For performance reasons suggest
uses monadic lazy lists (mllist
). This means that suggest
might miss some results if num
is not large enough. However, because suggest
uses monadic lazy lists, smaller values of num
run faster than larger values.
An example of suggest
in action,
example (n : nat) : n < n + 1 :=
begin suggest, sorry end
prints the list,
exact nat.lt.base n
exact nat.lt_succ_self n
refine not_le.mp _
refine gt_iff_lt.mp _
refine nat.lt.step _
refine lt_of_not_ge _
...
swap n
will move the n
th goal to the front. swap
defaults to swap 2
, and so interchanges the first and second goals.
The tfae
tactic suite is a set of tactics that help with proving that certain
propositions are equivalent.
In data/list/basic.lean
there is a section devoted to propositions of the
form
tfae [p1, p2, ..., pn]
where p1
, p2
, through, pn
are terms of type Prop
.
This proposition asserts that all the pi
are pairwise equivalent.
There are results that allow to extract the equivalence
of two propositions pi
and pj
.
To prove a goal of the form tfae [p1, p2, ..., pn]
, there are two
tactics. The first tactic is tfae_have
. As an argument it takes an
expression of the form i arrow j
, where i
and j
are two positive
natural numbers, and arrow
is an arrow such as →
, ->
, ←
, <-
,
↔
, or <->
. The tactic tfae_have : i arrow j
sets up a subgoal in
which the user has to prove the equivalence (or implication) of pi
and pj
.
The remaining tactic, tfae_finish
, is a finishing tactic. It
collects all implications and equivalences from the local context and
computes their transitive closure to close the
main goal.
tfae_have
and tfae_finish
can be used together in a proof as
follows:
example (a b c d : Prop) : tfae [a,b,c,d] :=
begin
tfae_have : 3 → 1,
{ /- prove c → a -/ },
tfae_have : 2 → 3,
{ /- prove b → c -/ },
tfae_have : 2 ← 1,
{ /- prove a → b -/ },
tfae_have : 4 ↔ 2,
{ /- prove d ↔ b -/ },
-- a b c d : Prop,
-- tfae_3_to_1 : c → a,
-- tfae_2_to_3 : b → c,
-- tfae_1_to_2 : a → b,
-- tfae_4_iff_2 : d ↔ b
-- ⊢ tfae [a, b, c, d]
tfae_finish,
end
Tag lemmas of the form:
lean
@[ext]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...
The attribute indexes extensionality lemma using the type of the
objects (i.e. my_collection
) which it gets from the statement of
the lemma. In some cases, the same lemma can be used to state the
extensionality of multiple types that are definitionally equivalent.
lean
attribute [ext [(→),thunk,stream]] funext
Those parameters are cumulative. The following are equivalent:
lean
attribute [ext [(→),thunk]] funext
attribute [ext [stream]] funext
and
lean
attribute [ext [(→),thunk,stream]] funext
One removes type names from the list for one lemma with:
lean
attribute [ext [-stream,-thunk]] funext
Also, the following:
lean
@[ext]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...
is equivalent to
lean
@[ext *]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...
The *
parameter indicates to simply infer the
type from the lemma's statement.
This allows us specify type synonyms along with the type that referred to in the lemma statement.
lean
@[ext [*,my_type_synonym]]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...
Attribute ext
can be applied to a structure to generate its extensionality lemma:
@[ext]
structure foo (α : Type*) :=
(x y : ℕ)
(z : {z // z < x})
(k : α)
(h : x < y)
will generate:
@[ext] lemma foo.ext : ∀ {α : Type u_1} (x y : foo α), x.x = y.x → x.y = y.y → x.z == y.z → x.k = y.k → x = y
lemma foo.ext_iff : ∀ {α : Type u_1} (x y : foo α), x = y ↔ x.x = y.x ∧ x.y = y.y ∧ x.z == y.z ∧ x.k = y.k
The reassoc
attribute can be applied to a lemma
@[reassoc]
lemma some_lemma : foo ≫ bar = baz := ...
and produce
lemma some_lemma_assoc {Y : C} (f : X ⟶ Y) : foo ≫ bar ≫ f = baz ≫ f := ...
The name of the produced lemma can be specified with @[reassoc other_lemma_name]
. If
simp
is added first, the generated lemma will also have the simp
attribute.
reassoc_of h
takes local assumption h
and add a ≫ f
term on the right of both sides of the equality.
Instead of creating a new assumption from the result, reassoc_of h
stands for the proof of that reassociated
statement. This prevents poluting the local context with complicated assumptions used only once or twice.
In the following, assumption h
is needed in a reassociated form. Instead of proving it as a new goal and adding it as
an assumption, we use reassoc_of h
as a rewrite rule which works just as well.
example (X Y Z W : C) (x : X ⟶ Y) (y : Y ⟶ Z) (z z' : Z ⟶ W) (w : X ⟶ Z)
(h : x ≫ y = w)
(h' : y ≫ z = y ≫ z') :
x ≫ y ≫ z = w ≫ z' :=
begin
-- reassoc_of h : ∀ {X' : C} (f : W ⟶ X'), x ≫ y ≫ f = w ≫ f
rw [h',reassoc_of h],
end
Although reassoc_of
is not a tactic or a meta program, its type is generated
through meta-programming to make it usable inside normal expressions.
tidy
attempts to use a variety of conservative tactics to solve the goals.
In particular, tidy
uses the chain
tactic to repeatedly apply a list of tactics to
the goal and recursively on new goals, until no tactic makes further progress.
tidy
can report the tactic script it found using tidy?
. As an example
example : ∀ x : unit, x = unit.star :=
begin
tidy? -- Prints the trace message: "intros x, exact dec_trivial"
end
The default list of tactics can be found by looking up the definition of
default_tidy_tactics
.
This list can be overriden using tidy { tactics := ... }
. (The list must be a list of
tactic string
, so that tidy?
can report a usable tactic script.)
Unfold coercion-related definitions
Similar to existsi
. use x
will instantiate the first term of an ∃
or Σ
goal with x
.
Unlike existsi
, x
is elaborated with respect to the expected type.
Equivalent to refine ⟨x, _⟩
.
use
will alternatively take a list of terms [x0, ..., xn]
.
Examples:
example (α : Type) : ∃ S : set α, S = S :=
by use ∅
example : ∃ x : ℤ, x = x :=
by use 42
example : ∃ a b c : ℤ, a + b + c = 6 :=
by use [1, 2, 3]
example : ∃ p : ℤ × ℤ, p.1 = 1 :=
by use ⟨1, 42⟩


There are no working premium support packages available for the current organization.
{{ ::plan.description }}


Ruth Bader Ginsburg hospitalized for chills and fever, Supreme Court says
by Morgan PhillipsSupreme Court Justice Ruth Bader Ginsburg was admitted to Johns Hopkins Hospital on Friday night after experiencing chills and a fever, the Supreme Court said Saturday night.
Ginsburg, 86, was initially evaluated at Sibley Memorial Hospital in Washington, D.C., before being transferred to Johns Hopkins for further evaluation and treatment of any possible infection, the Supreme Court said in a press release.
Her symptoms have abated after intravenous antibiotics and fluids and she is expected to be released from the hospital as early as Sunday morning, according to the release.
Ginsburg has suffered a number of hospital stints recently.
RUTH BADER GINSBERG MISSES SUPREME COURT ARGUMENTS DUE TO ILLNESS
She missed oral arguments before the high court on Nov. 13 -- which she almost never does -- due to a stomach bug.
Ginsburg has also had two separate bouts with cancer in the past year. Her recovery from lung cancer caused her to miss court sessions in January, her first time doing so in her quarter-century as a justice.
CLICK HERE TO GET THE FOX NEWS APP
In August, she had radiation treatment for a tumor on her pancreas.


WITNESS LIST Public Health Committee March 23, 2005-12:00A HB 1015 For: Burney, PhD, J. Paul (Texas Psychological Association) McPherson, Dr. Bob (Texas Psychological Association) On: Aerne, Melissa (Sunset Commission) Hernandez, Ph.D., Arthur (Texas State Board of Examiners of Psychologists) Shute, Geoffrey M. (Self and Texas Association of Psychological Associates) Registering, but not testifying: On: Lee, Sherry (Tx. St. Bd. of Examiners of Psychologists) HB 1086 For: Carter, Janis (Texas Funeral Directors Assoc) Gilligan, T. Scott (Texas Funeral Directors Association) Smith, Scott (Texas Funeral Directors Assn) Against: Bates, Jim (Funeral Consumers Alliance of North Texas) Beresford, Chip (Self) Hankins, Lamar (Funeral Consumers Alliance of Texas) Wendell, Ware (Self) Wolens, Steven (Self and Certain plaintiffs in suit against SCI funeral homes) On: Robbins, O.C. (Chet) (Texas Funeral Service Commission) Registering, but not testifying: For: Hughes, Caressa (Service Corporation International) Rogers Jr, Johnnie B. (Service Corporation International) HB 1135 For: Henning, Lori (Texas Assoc. of Goodwills) Kafka, Bob (Adapt of TX) Kern, Diana (Self and National Alliance for the Mentally Ill of TX (NAMI Texas)) Schwartz, Jonas (Advocacy Incorporated) Suiter, Kim (National Multiple Sclerosis Society) On: Casey, Dianne (Health and Human Services Commission) Hawkins, Albert (Health and Human Services Commission) Lottmann, Larry (Dept Assistive and Rehab Services) Registering, but not testifying: For: Banning, Tom (Tx Academy of Family Physicians) Borel, Dennis (Coalition of Texans w/ Disabilities) Elrod, Susanne (Texas Council of Community MHMR Centers) Holcomb, John (Self and Texas Medical Association) Kolodzey, Patricia (Texas Hospital Association) Maxwell, Susan M (Texas Council for Developmental Disabilities) Sabo, Jason (United Ways of Texas) Vasek, Heather (Texas Association for Home Care) Woolbert, Lynda (Coalition for Nurses in Advanced Practice) HB 1155 For: Farr, Linda (Texas Dietetic Association) Montgomery, Cathy (Self) Poinsett, Hawley (Texas Dietetic Association) Ricks, Felicia (Texas Dietetic Association Renal Practice Task Force) On: Peterson, Debbie (Dept of State Health Services Professional Licensing) Trost, Amy (Sunset Commission) Registering, but not testifying: For: Hooser, Greg (Texas Dietetic Association) HB 1435 On: Trost, Amy (Sunset Commission) Zukowski, Dr. Jim (Texas State Board of Podiatric Medical Examiners) Registering, but not testifying: For: Hanna, Mark J. (Texas Podiatric Medical Association) On: Alonzo, Janie (Tx St Bd of Podiatric Medical Examiners) Makan, Hemant (Texas State Board of Podiatric Medical Examiners) HB 1604 On: Harris, Geraldine R. (Texas Dept. of State Health Services / Vital Statistics Unit) Registering, but not testifying: For: Banda, Jennifer (Texas Hospital Association) HB 1771 For: Hernandez, George B. (Bexar County Hospital District) Holcomb, John (Self and Texas Medical Association) SvadLenak, Steve (Texas Association of Public and Non-Profit Hospitals) Tonn, Larry (Tx Assoc. Voluntary Hospitals, Dallas Medical Resource) Turcotte, Michael (Gentiva) Vasek, Heather (Texas Association for Home Care) Willson MD, Charles F. (Texas Medical Association) Against: Bowers, Chris (Superior Health Plan) Brown, Bess (Self) Buckwold, Dr. Fred (Evercare of Texas, LLC) Rossberg, Cathy (Amerigroup) Sullivan, Sandy (Evercare) On: Borel, Dennis (Coalition of Texans with Disabilities) Brown, Will (AARP-Texas) Camacho, Jose E. (Tx. Assn of Community Health Centers, Inc.) Coleman, Pam (Tx Health and Human Services Commission) Gibson, Linda (Comptroller's Office) Hawkins, Albert (Health and Human Services Commission) Horton, Colleen (Tx. Center for Disability Studies) Kafka, Bob (ADAPT of Tx) Palmer, David (HHSC) Registering, but not testifying: For: Banning, Tom (Tx Academy of Family Physicians) Capelo, Jaime (Pediatrix Medical Group) Crowe, Michael (Texas Assisted Living Association) Cutrer, Dr. Jennifer (Parkland Health and Hospital System) Hillier, R. King (Harris County Hospital District) Hooser, Greg (Scott and White Hospital and Clinic) Jamison, Mazie M. (Children's Medical Center Dallas) Kolodzey, Patricia (Texas Hospital Association) Kroll, Carrie (Texas Pediatric Society) Lee, Donald (Texas Conference of Urban Counties) Moreno, Gabriela (CHRISTUS Health) Roy, Tom E. (JPS Health Network) Woolbert, Lynda (Coalition for Nurses in Advanced Practice) On: Johnson, Gary (Comptroller's Office) Murphree, Susan (Advocacy Inc.) Sanchez, Joe M. (AARP - Texas) HB 2680 For: Ellzey, M.D., Robert F. (Self and Travis County Medical Society, Retired Physicians of Texas) Gunn, Cindy (Memorial Hermann Healthcare System) Orr, Fred (Christ's Family Clinic) Price, M.D., P. Clift (Texas Medical Association) On: Garanflo, Jaime (Tx State Board of Medical Examiner's) Peterson, Debbie (Dept of State Health Services Professional Licensing) Registering, but not testifying: For: Austin, Myra (CHRIST'S FAMILY CLINIC) Camacho, Jose E. (Tx. Assn of Community Health Centers, Inc.) Moreno, Gabriela (CHRISTUS Health) Young, Jenny (Texas Dental Association)


jME3 supports several types of special effects: Post-Processor Filters, SceneProcessors, and Particle Emitters (also known as particle systems). This list contains screenshots and links to sample code that demonstrates how to add the effect to a scene.
com.jme3.effect.ParticleEmitter
class for all Particle Systems. com.jme3.post.FilterPostProcessor
class and several com.jme3.post.filters.*
classes (all Filters have *Filter
in their names). SceneProcessor
classes in various packages, including e.g. com.jme3.shadow.*
and com.jme3.water.*
(SceneProcessor have *Processor
or *Renderer
in their names).public class MyGame extends SimpleApplication { public void simpleInitApp() { ParticleEmitter pm = new ParticleEmitter("my particle effect", Type.Triangle, 60); Material pmMat = new Material(assetManager, "Common/MatDefs/Misc/Particle.j3md"); pmMat.setTexture("Texture", assetManager.loadTexture("Effects/spark.png")); pm.setMaterial(pmMat); pm.setImagesX(1); pm.setImagesY(1); rootNode.attachChild(pm); // attach one or more emitters to any node } }
public class MyGame extends SimpleApplication { private BasicShadowRenderer bsr; public void simpleInitApp() { bsr = new BasicShadowRenderer(assetManager, 1024); bsr.setDirection(new Vector3f(.3f, -0.5f, -0.5f)); viewPort.addProcessor(bsr); // add one or more sceneprocessor to viewport }
public class MyGame extends SimpleApplication { private FilterPostProcessor fpp; // one FilterPostProcessor per app private SomeFilter sf; // one or more Filters per app public void simpleInitApp() { fpp = new FilterPostProcessor(assetManager); viewPort.addProcessor(fpp); // add one FilterPostProcessor to viewPort sf = new SomeFilter(); fpp.addFilter(sf); // add one or more Filters to FilterPostProcessor }
The jMonkeyEngine's "SeaMonkey" WaterFilter simulates ocean waves, foam, including cool underwater caustics. Use the SimpleWaterProcessor (SceneProcessor) for small, limited bodies of water, such as puddles, drinking troughs, pools, fountains.
See also the announcement with video.
Thanks for your awesome contributions! Keep them coming!
Particle emitter effects are highly configurable and can have any texture. They can simulate smoke, dust, leaves, meteors, snowflakes, mosquitos, fire, explosions, clusters, embers, sparks…
See also:


What Is a Flow?¶
A flow is a collection of tasks which should execute in a specific sequence.
Modeling Flows: Flows as DAGs¶
In MissionControl, we think about flows as Directed Acyclic Graphs, or DAGs. For more on DAGs, see https://en.wikipedia.org/wiki/Directed_acyclic_graph. In our DAG the nodes are our tasks; the edges define the sequence.
Modeling flows as DAG allows us to define many types of flows. For example, we can define a flow that is a simpler linear sequence:
Todo
- MAKE LINEAR FLOW GRAPHIC
Or, we can define a flow that has branches that run in parallel:
Todo
- MAKE PARALEL FLOW GRAPHIC
Representing Flows¶
So now we know how we can model flows. But how can we represent a flow?
One way to represent a flow is as a drawing. For example:
Todo
- MAKE FLOW DRAWING
Ideally we could make a drawing, and then show that drawing to a computer and have it run our flow. But one of the problems with drawings is that they are hard for computers to understand.
Note
Am exercise for the enterprising reader: make a tool that converts a drawing of a flow into a text representation.
Since we want to make our flows readable by computers, we use other representations.
One way we can represent a flow is as a list of tasks and edges.
Another way we can represent a flow is as a list of tasks and edges.
Going From a Drawing to a Flow¶
How do we go from a drawing to a running flow? We break it down.
 One way is to make a complete skeleton of our flow, and then fill it in. Another is way is to add tasks one at a time, testing them and building them up along the way.
Both approaches have merits, and you can even use a combination of the two.
The key thing is not to get bogged down! Remember, you can always change your flow later. So just write as much as you know now, and fill in the rest later.
One way is to start by making a skeleton flow that represents the sequencing of our flow. In this skeleton flow our tasks don’t do anything yet. They just print out a message.
This skeleton gives us a starting point. We can check that the sequence of our flow works as expected. And then we can fill logic in as needed.
The next step is implementing a task.


Goto the Slack Workspace and register as a user..
To export conversation histroy of any channel there type:
/export-conversation


The programm finds the geographic, Gauss-Krueger, or UTM coordinates of a point, indicated in the map. The map must already exist as a '*.bmp','*.gif', '*.tif', '*.jpg' file, '*.wmf', or '*.emf file, or on the clipboard. It can then be imported. The margins of the map are typed into the relevant fields either as geograhic, Gauss-Krueger, or UTM-coordinates. If data points are marked on the backside of a map, the map is drawn back to front.
Procedure:
1) Decide in the menu 'import map', whether the map is imported from a
data carrier or from the clipboard.
2) Indicate in the menu 'marking of data locations', whether the data
points are marked on the front side or on the backt.
3) Type the coordinates of the margins in the relevant fields.
4) Click on the data points.
5) Mark the fabric type with 'p' for planes or 'l' for linears, type azimuth and dip
angle.
6) Click on 'terminate input' when all points are clicked.
7) Create the map by clicking on "Plot".


View Evaluation Tool Results
Location of confusion_matrix.html
Location of samples
Location of images


tree change temperature climate MAT forest tree,ctrl IAP‐DGVM < global CLM‐CNDV Figure regions coverage changes ecosystems fractional areas ecosystem vegetation Global responses (Figure GPP boreal MAP case different grid {border-style carbon decreased eco forests increasing px;} sensitivity tropical warming #ffffff;} CLM‐CNDV, IAP‐DGVM, effects increased models cases cells distribution precipitation approximately decreasing sensitive soil Biology, Change forests, larger simulated concentration establishment growth response used However, relationship CLM‐CNDV. China change, dynamic i.e., influences positive shown simulation °C, IAP‐DGVM. Model National area‐averaged dependence differences investigate led models, models. > area arid conditions especially results semiarid standard year Atmospheric PFTs Science Wang, Zeng, control cooling coupled deviation line maximum plant px; seven temperate tests tree; using {font-family (e.g., CLM Land MAT′ Vegetation Zhu, atmospheric change. font-size future however, individual mean moisture primary significant structure terrestrial tree, trees types value work Academy Central Foundation Natural Science, Sciences, Sitch, Song, United amplitude annual double; explore negative nitrogen rate reduced respiration similar simulations, temperature, th, years Broadleaf Center Chinese Community DGVMs Dai, Furthermore, Li, Sciences States Williams, accounted biomass border-color border-width core determined factor fertilization gross important influencing large largely model photosynthesis population precipitation, production range reached reduction revised showed solid; species tree,ctrl, tree,ctrl; warming, work, zones {font-style {font-weight (a, (c, Amazonian America, Bonan, Climate Climate, Comparison Costa, DGVM Dickinson, Dynamic Ecology Ecology, Evaluation Forest Lomas, Notaro, Prentice, Qian, Similar accordance appeared blue bold change: concentration. considered. cooling, courier; current data deciduous decreased, direct distributed drought ecological em; evergreen following form greater higher impact influence lead mainly max net occurred opposite optimal partly percentiles, peripheral productivity pt;} rates regions, relationships respectively respiration, result shows stronger tree| vital vs. water western


Todo List
Scenario
- Pass the core reference to new experiment objects rather than use the singleton.
- Pass a reference in upon construction rather than using the singleton.
- Use a reference to the core rather than the singleton.
- Base on default identity setting in core
Documentation generated on Sat, 23 Oct 2010 17:23:43 -0400 by phpDocumentor 1.4.3


PillowChick sets up shop at Nictus 29 Nov 2019, 10:29 by Emmency Nuukala Home \ Entertainment \ PillowChick sets up shop at Nictus - New Era Live


This is a Bootstrap based theme developed by the Salesforce.com Foundation's Business Applications team. The aim is to provide a solid and complete theme for Bootstrap that matches the SFDC Salesforce1 styleguide.
The general look and feel is inspired by the SFDC Styleguide. There is some intention of building theme variations for different application contexts (visualforce, salesforce1, chatter), but this work has not been done at this time.
The Proxima Nova Soft fonts are not included in this repository. To match the SFDC styles you will need to include this font in your page.
To use the theme you just need to include the dist/
folder in your project and include bootstrap.css
or bootstrap.min.css
in your page. For use inside of a VisualForce page you may need to use the namespaced CSS in bootstrap-namespaced.css
.
You can download the theme using bower:
bower install bootstrap-sf1
Or you can download the zip.
You will need:
Things never to do:
dist/
directlypages/
or the index.html
file directlyless/generated
folder directlyThese files are generated automatically and your changes will be overwritten. You have been warned. :)
First clone the repo and navigate into the directory:
git clone https://github.com/SalesforceFoundation/bootstrap-sf1.git
cd bootstrap-sf1
Next
npm install
bower install
There are a number of files that are generated for you as you make changes to the less files. To facilitate this process start the grunt watch machinery with:
grunt serve
This will also start up a local webserver at http://localhost:8000. As you edit Less files or templates Grunt will automatically compile the CSS and HTML for the docs so long as you have grunt serve
running.


Wednesday, 15th March 2056
I am a fast learning, hard working and passionate Web Developer. Ideally, I am looking for a progressive working environment to continue my exciting learning journey.
While being new to the tech industry, I bring a wealth of experience, skills and talents gained through my previous employment phases. I have a mature approach to the professional workplace, balanced with a disarming sense of humour. I get along with people easily, through my experience in working in Government, trade and retail workplaces.
As a Junior Web Developer, I believe that high levels of productivity, and strong workplace satisfaction, are directly correlated with personal well-being and opportunities for continuous learning.
Through my time at the Enspiral Dev Academy, I’ve been able to achieve a seismic shift in my career journey, into the tech industry. With my creative arts and academic background, I’ve found found a new set of tools to explore and express myself with.
With the new web dev tools I have learnt, I love building digital things, where there’s always something new to learn. This has felt like a natural progression from my interest in creating things with my hands.


#731 l_ous
laborious
lascivious
lecherous
libelous
licentious
litigious
loquacious
ludicrous
luminous
luscious
lustrous
luxurious


ABSTRACT
Khrutba V.A., Ziuziun V.I., Lysak R.S. Formation of a System of Criteria for Assessing the Environmental Impact in Construction and Reconstruction Projects of Critical Infrastructure. Visnyk National Transport University. Series «Technical sciences». Scientific and Technical Collection. - Kyiv: National Transport University, 2021. - Issue 1 (48).
In the study, based on the existing approaches to the assessment of mental space in the project management environment, a model of mental space for the implementation of transport safety projects was formed.
The purpose of the work is to create a system model of the formation of mental space in the management of security projects of transport enterprises to increase the efficiency of their implementation.
Research methods - project and program management methodologies; mechanisms of set theory, system and process analysis.
The developed system model includes the mental space of the security project; the mental space of the project manager / project team, to be determined by the general policy of safety management of the enterprise and is formed by the mental space of the transport enterprise; the mental space of stakeholders is defined as the mental space that is formed by the general attitude to ensuring the safety of the transport industry; the mental space of mobile content / environment is determined by the zonal culture of transport safety that exists in a particular region. This comprehensive approach allows us to move towards taking into account all the important components in the management of transport safety and especially in transport companies.
The results of the article in the implementation of the procedure of forming a mental space in the management of security projects of transport enterprises to improve their efficiency can be implemented.
Predictive assumptions for the development of the object of study - the development of a method of forming a mental space in the management of security projects of transport enterprises.
KEY WORDS: PROJECT, PROJECT MANAGEMENT, MENTAL SPACE, TRANSPORT ENTERPRISE, SECURITY, SYSTEM MODEL.
REFERENCES
AUTHOR
Khrutba Viktoriia Alexandrovna, Doctor of Science, National Transport University Head of the Department of Ecology and Safety of Vital Functions, e-mail<EMAIL_ADDRESS>tel. +380935372915, Ukraine, 01010, Kyiv, Omelyanovch-Pavlenko st. 1, of. 312, orcid.org/0000-0002-8121- 2042.
Ziuziun Vadym Ihorovych, PhD, National Transport University, Associate Professor of the Department of Ecology and Safety of Vital Functions, e-mail<EMAIL_ADDRESS>тел. +380939834845, Ukraine, 01010, Kyiv, Suvorova str. 1, of. 312, orcid.org/0000-0001-6566-8798.
Lysak Roksolana Stanislavivna, Assistant Lecturer of the Department of Ecology and Safety of Vital Functions, National Transport University, e-mail<EMAIL_ADDRESS>tel. +380979756341, Ukraine, 01010, Kyiv, Omelyanovch-Pavlenko st. 1, of. 312, orcid.org/0000-0002-2776-5623.
REVIEWER
Bushueva N.S., Ph.D., Engineering (Dr.), professor, Kyiv National University of Construction and Architecture, Head of the department of project management, Kyiv, Ukraine.
Hryshchuk O.K., Ph.D, professor, National Transport University, Vice-Rector for Academic Work, Kyiv, Ukraine.
Article language: Ukrainian
Open Access: http://publications.ntu.edu.ua/visnyk/48/358-367.pdf
Print date: 15.03.2021
Online publication date: 05.04.2021


How much do you get paid per hour?
How many hours a day do you work?
How many days per month do you work
How much tax do you pay?


|
Game of Fifteen - Extended
1.0.0
Documentation of extended version of "Game of Fifteen".
|
View responsible for showing all Blocks that takes part in the game. More...
#include <blocks_view.h>
Public Slots | |
| void | gameStartedHandler (const std::vector< std::shared_ptr< Block< BlockLayoutItem >>> &blocks, const size_t &level) |
| Handles the new game signal. More... | |
| void | blockSwapedHandler (Block< BlockLayoutItem > &a, Block< BlockLayoutItem > &b, const std::shared_ptr< Move > &move) |
| Handles the swapped blocks signal. More... | |
| void | puzzleSolvedHandler () |
| Handles the puzzle solved signal. More... | |
Signals | |
| void | blockClicked (const Position &position) |
| Emitted whenever displayed Block has been clicked. More... | |
Public Member Functions | |
| BlocksView (QWidget *parent=nullptr) | |
| Creates the view. More... | |
| virtual | ~BlocksView ()=default |
| The default destructor. More... | |
Protected Member Functions | |
| void | mousePressEvent (QMouseEvent *event) |
| Handles mouse pressed events that origin from the blocks view. More... | |
View responsible for showing all Blocks that takes part in the game.
|
explicit |
Creates the view.
| parent | The Qt's parent object. |
|
virtualdefault |
The default destructor.
|
signal |
|
slot |
|
slot |
Handles the new game signal.
| blocks | The array of pointers to all Blocks that creates the board. |
| size | The edge size of a board (i.e. 4 in case of board created for 16 blocks) |
|
protected |
Handles mouse pressed events that origin from the blocks view.
| event | The mouse event. |
|
slot |
Handles the puzzle solved signal.


Top 5 Best Mobile Phone Under 10k
When you buy a phone what did you want?
- is it that I want a phone that never hangs but every device has some problem | Every phone hangs | And even under 10k mobile are hang much more than an expensive phones? - So, this is not possible.
But it is possible that you can buy a phone that hangs very rarely.
We compared all the phone under 10k and we will find some phone that is better than other are given below -
1.Micromax IN 1 - All Rounder
- It has 48megapixel camera.
- G80 processor [ Entry level Gaming Processor ]
- 16.94 cm (6.67 inch) Full HD+ Display
- 5000 mAh Lithium Polymer Battery
- 18w Fast Charging
2.Realme narzo 30a - Performance Beast under 10k
- It has G85 - [ Entry level Gmaing processor ] - ( Best Processor under 10k )
- 6000 mAh Battery
- 16.54 cm (6.51 inch) HD+ Display
- 13MP + 2MP | 8MP Front Camera
- 18w Fast Charging
3.Redmi 9 prime - Front Gorila Glass
- 16.59 cm (6.53 inch) Full HD+ Display
- G80 processor [ Entry level Gaming Processor ]
- 13MP Rear Camera | 8MP Front Camera
- 5020 mAh Battery
- 18w Fast Charging
4.Realme C25 - Realme Ui 2.0
- 16.51 cm (6.5 inch) HD+ Display
- 13MP + 2MP + 2MP | 8MP Front Camera
- 6000 mAh Battery
- MediaTek Helio G70 Processor
- 18w Fast Charging
5.Realme narzo 20a - Qualcomm Snapdragon 665 Processor
- Qualcomm Snapdragon 665 Processor
- 16.51 cm (6.5 inch) HD+ Display
- 12MP + 2MP + 2MP | 8MP Front Camera
- 5000 mAh Lithium-ion Battery
- 18w Fast Charging
Advice - I shall advice you to buy Samsung phone if you did not play games because their software are very good as compared to other smart phone companies in the market.


DIRECTED BY: Martin Scorsese WRITTEN BY: Paul Schrader, based upon a novel by Joe Connelly CAST: Nicolas Cage, Ving Rames, Tom Sizemore, John Goodman, Patricia Arquette
MPAA: Rated R for gritty violent content, drug use and language. Runtime: USA:120
"Saving someone's life is like being in love. It's the best drug in the world. You feel like God was in you. And why deny it? Why deny that for a moment God was you"
RATING: 10/10 - BEST PICTURE - #6
"The night started out with a bang. All the elements were in place for a long weekend: heat, humidity, moonlight. I was good at my job. There were periods when my hands moved with a speed and skill beyond me. But during the last year I started to loose that control. Things had turned bad. I haven't saved anyone in months. I have come to believe in such things as spirits leaving the body and not wanting to be put back. I grew up in this neighborhood. I worked here most as a paramedic and it had more ghosts per square foot than any other. Rose's ghost was getting closer. I just needed a good night's sleep and a couple of days off. It was six months since I lost Rose. Homeless. Asthmatic. 18 years old. I used to block bad calls out, but she wouldn't let go. And now she came to bare witness for all of them -- all that have been lost. I've always had nightmares, but now the ghosts didn't wait for me to sleep. They were part of the job- the eyes of a corpse, the screams of a loved one. After a while I came to understand that my role was less about saving lives, but about bearing witness. It was enough that I simply showed up. Except with Rose..." © Paramount Pictures
It is the early 1990's and New York has not yet undergone its renaissance of recent years. Sirens screaming and lights flashing, a New York City ambulance speeds through the night. Its drivers are paramedics working the graveyard shift -- men who come face-to-face with the dead and the dying on a daily basis. Burnt out from one too many nights on the job, they are nearly as broken as the bodies they haul through the streets. What keeps them going is their caustic sense of comedy, and an acrid view of a world which seems to have its surreal epicenter in Manhattan. Frank (Nicolas Cage) is among them. He has been doing this for 5 years and it is both his salvation and his doom, his dream and his nightmare. When he saves someone's life everything inside him glows and he feels as light as a feather. It's another thing when he looses a patient.  Tormented by horrible nightmares and haunted by ghosts of the people that he didn't manage to save, he reaches the very brink of spiritual collapse and redemption. We follow him and his colleges during 56 hours of their lives and share the experience of being a paramedic. Among them is the angry Tom (Tom Sizemore), the holy Marcus (Ving Rames) and the tiered Larry (John Goodman).
This is the long awaited comeback of the respected and acclaimed director Martin Scorsese, and I can assure you that it has been worth waiting for. Scorsese has always been a controversial director that created some of the best films Hollywood had to offer over the years. 'Bringing Out the Dead' doesn't have his most obvious trademarks, since this is not a mafia-fable, there is no particular violence or gore, and Robert De Niro is not in it. But artistically this is certainly 'A Martin Scorsese Film'. There is no particular story or character development. No melodrama. No climatic ending. This is reality. There is no question about it. It is 56 hours of a life. Scorsese, along side with Paul Schrader ('Taxi Driver') creates incredible characters that are so real, so human and vulnerable that we connect with them immediately. They live in a world, unknown to us. A world of eternal night, constant death, blood and suffering. There are periods of depression, a feeling of worthlessness, when they are not saving anyone. They feel like messengers of death. Confused, tormented, haunted, angry, they are all searching for someone to blame.  All they feel is a constant longing for peace -- for that long forgotten feeling of closing the eyes and simply float away. They are not rescuers. They are not saviors. Their job is simple -- they are brining out the dead. This is a wildly surreal film. There is a bizarre feeling of a world within a world. Scorsese unravels his dark vision and paints a devastating picture of madness, paranoia, fear and death that form a void, a darkness that swallows you and doesn't let go. His film is explosive, expressive, fast paced and haunting. At times Scorsese is resorting to a pitch dark comedy, without loosing his point. "Hold this. If you let go, I swear, I won't kill you," Frank warns a suicidal character with another unexpected, throwaway punchline characteristic of all film's dialogue. But mostly Scorsese does what he does best -- displaying the pure, na k their frustrations, by channeling them into something else. Frank and his friends have all gone mad in their own direction. Larry races from diner to fast food joint, dreaming of the suburbs.  Marcus survives by putting his trust and hope in faith, a belief that all the death, misery and suffering happen according to God's divine and unknown plan. But none of their coping mechanisms work for Frank. For him life is just a void, an existence in a never ending darkness from which there is no escape.
Every performance is so controlled, so perfect, so real that you never question its authenticity. Nicolas Cage, an actor that has been accused of being a 'paycheck player', choosing money instead of art, shows his talent in a soulful and committed performance as the tortured and half-crazed paramedic. He mixes downcast periods of gloomy introspection with episodes of wild, lunatic abandon. At times his bloodshot, tormented eyes portray more sorrow and depth than any words that he is pronouncing. This is certainly Cage's best performance since 'Leaving Las Vegas'. Tom Sizemore ('Heat', 'Saving Private Ryan' ) is equally magnificent. He releases so much energy, so much emotion and power into his performance that he looks more like a ticking bomb rather than a person. Ving Rames ('Entrapment' ) gives a brilliant comic performance as the 'holy medic'. There are times when before resurrecting someone on the streets he (in a high pitched voice) asks God's forgiveness for "these sinners". Visually and technically this film is above perfect. Robert Richardson's cinematography is rich and inventive, employing some crazy shots as the camera turns the world upside down. Thelma Schoonmaker binds Richardson's shots together with her explosive editing, fast motion, flashing lights and neon glow. The music is provided by Elmer Bernstein's bizarre, eclectic score and some wisely inserted songs by Van Morrison and The Clash, among others. When all those elements are combined, they create an almost carnival atmosphere of light and shade, speed and violence that really gets under the skin. New York has never looked so dark before. The streets are empty, lit only by the pale moon, neon glow and flashing red lights of an ambulance. The only inhabitants are shadows, filth and dust. In other words, Scorsese has created a wildly surreal, dark and effectively paranoid motion picture, which is the director's best work since 'Goodfellas' (1990). Remember: This is NOT a light, entertaining popcorn-film or a feel-good movie. It is an incred i tale, which is nothing less than a powerful and emotionally devastating cinematic experience, created by the maestro of shadows and light.
The review above was posted to the
rec.arts.movies.reviews newsgroup (de.rec.film.kritiken for German reviews).
The Internet Movie Database accepts no responsibility for the contents of the
review and has no editorial control. Unless stated otherwise, the copyright
belongs to the author.
Please direct comments/criticisms of the review to relevant newsgroups.
Broken URLs inthe reviews are the responsibility of the author.
The formatting of the review is likely to differ from the original due
to ASCII to HTML conversion.
Related links: index of all rec.arts.movies.reviews reviews


Hertz is one of the largest car rental companies in the world. It has over 10,000 corporate and franchisee locations. Last week, I tested the usability of the hertz.com website on a computer. This week, a usability test was conducted to determine the ease of use of the website on mobile devices https://www.hertz.com for older adults. This blog provides a summary of this test and its results.
Summary of the test
Purpose and methods used
The purpose of this test was to test the Hertz website on a mobile device to see how user friendly it is for older adults. The test was conducted on April 30 through May 2, 2020 via Zoom sessions due to the Covid-19 outbreak. Sessions were recorded with the users’ permission.
Each user was asked to log onto the site on a mobile device and I read a script describing that we were testing the usability of the Hertz website. Each user was asked if they had ever used a website to rent a car, and if they had used the Hertz website. The users were asked to perform three tasks and were told to say their thoughts out loud as they performed the tasks. The following tasks were included in the test:
- Find Hertz locations near you
- Assume you are making a one-and-a-half-week trip to Seattle.
- Find out what offers are available for AAA members.
After the test, I looked back at the videos and noted how much time and the number of actions performed on each task. The full test script can be found here.
Number and demographic summary of participants
In all, there were three participants. Two-thirds identified as male and the average age was 64.7. Two-thirds had previously used a website to rent a car, and the same users had used the Hertz website before. One of those users said it had been a significant amount of time since using the Hertz website.
Results summary
Task 1
In the first task, they were asked to find Hertz locations near them.
The following charts presents the number of steps and time it took the users to complete the task.
Like my previous test using a computer, users gravitated to the reservation functionality to find locations even though the locations feature was a menu item.
Each user approached this task in different ways. Using the menu, user 1 quickly found locations in 32 seconds and four steps.
User 2 spent almost ten minutes trying to find a location using the pickup locations functionality in the reservation section of the home page. They tried using the names of local cities and zip codes which brought up either no results or locations not near their home. At one point, it displayed locations in other states and foreign countries. They felt like the location feature wasn’t done well and that it was surprisingly difficult. They mentioned that they would likely go to another rental car company because of the poor performance of this feature.
Also using the pickup feature, user 3 was able to find a location near their home and finish the task in just over two minutes and nine steps. However, their results were limited to a single location and they didn’t receive information about other locations near them
Task 2
In the second task, the users were asked to make a week and a half reservation and figure how much it would cost.
The following charts presents the number of steps and time it took the users to complete the task.
The experience of people in task two was also very similar to using a computer. Because the reservation feature is so prominent on the home page, they were automatically focused on it.
Users one and three had a similar experience finishing the task in about two and a half minutes. User two took almost nine minutes to complete the task due to difficulty finding a location. Both users one and two noted that you couldn’t clear the reservation information to allow the user to start over. This made the more cumbersome to use. In the end, all the users thought it was a reasonable experience.
Task 3
In task three, the users were told to find what offers were available for AAA members.
The following charts presents the number of steps and time it took the users to complete the task.
User three had no difficulty with this task. They found AAA deals in eighteen seconds and three steps. User one, initially tried to find the information using the menu but couldn’t locate anything about AAA. They then tried the search feature but didn’t find the results they were looking for. They went back to the menu and found deals under the “Rent” sub-menu. Oddly when they returned to the main menu, “Deals” showed up as an option. User three tried the menu but didn’t find anything about deals so they used the search feature three times using different criteria and didn’t find what they were looking for and gave up after about four minutes and eighteen steps.
Summary of issues found and next steps
Issues found
The experience was similar to the prior group who used computers. For both task one and three, the users on both types of devices gravitated towards the reservation section instead of the menu. In general, they all recognized the hamburger icon as the menu; however, they rarely went to it making it harder to find things.
Unlike on the computer, the deals option didn’t show up in the menu unless they clicked on the “Rent” submenu first. Because of the difficulty in finding the menu option for “Deals” users spent a lot of time searching for AAA deals.
Suggested solutions and next steps
As in the prior test, I would recommend a different use of color due to a very bland light on light website. This might help balance the reservation section with the menu and other options on the site.
I would also add some features like a clear button on the reservation section to make it easier for users to start over. The other thing would be to put a hyperlink in the reservations section for locations near me. That would highlight that the feature exists without having to use the menu.


UTILIZATION AND VIEWS OF AVAILABLE HEALTI! CARE AMONG RESIDENTS IN THREE POVERTY NEIGHBORHOODS
IN PITTSBURGH, PENNSYLVANIA
By Earl Donald Hollander B.A., Yeshiva University, 1957
M.S., Simmons College, 1960
Submitted to the Graduate Faculty in the School of Social Work in partial fulfillment of the requirements for the degree of
Doctor of Philosophy
University of Pittsburgh 1970
Reproduced with permission of the copyright owner. Further reproduction prohibited without permission.


Create an instance of the class that will use the named test method when executed. Raises a ValueError if the instance does not have a method with the specified name.
Fail if the two objects are unequal as determined by their difference rounded to the given number of decimal places (default 7) and comparing to zero.
Note that decimal places (from zero) are usually not the same as significant digits (measured from the most signficant digit).
Fail if the two objects are unequal as determined by their difference rounded to the given number of decimal places (default 7) and comparing to zero.
Note that decimal places (from zero) are usually not the same as significant digits (measured from the most signficant digit).
Fail if the two objects are equal as determined by their difference rounded to the given number of decimal places (default 7) and comparing to zero.
Note that decimal places (from zero) are usually not the same as significant digits (measured from the most signficant digit).
Fail if the two objects are equal as determined by their difference rounded to the given number of decimal places (default 7) and comparing to zero.
Note that decimal places (from zero) are usually not the same as significant digits (measured from the most signficant digit).
Fail if the two objects are equal as determined by their difference rounded to the given number of decimal places (default 7) and comparing to zero.
Note that decimal places (from zero) are usually not the same as significant digits (measured from the most signficant digit).
Fail if the two objects are unequal as determined by their difference rounded to the given number of decimal places (default 7) and comparing to zero.
Note that decimal places (from zero) are usually not the same as significant digits (measured from the most signficant digit).
Returns a one-line description of the test, or None if no description has been provided.
The default implementation of this method returns the first line of the specified test method’s docstring.


PREPARE & BE READY
RISK
BACKGROUND
PREPARE
SUBSCRIBE
ABOUT US
Sign-up to receive a risk alert
Receive an SMS alert if the risk level changes to High or Extreme:
At your location.
Across any location/s in the Greater Melbourne region.
To update your preference, please
click here


"With a presence of more than five decades in the textile industry, Darshan Valji is one of the top players in this segment and has emerged as a clear leader in the Corporate, Industrial & School Uniform segment. With a wide range of varied types of fabrics, sold under the brand name ”Valji”, the company’s fabrics are always favored over others when it comes to quality, designs & patterns"
100 years back Shri Tekchand Himatmalji Kothari came to Mumbai from a remote village called Bagol in Rajasthan with a dream of realizing his potential in this city. Initially to sustain he worked in various firms in the city which also gave him a wider perspective and a deep understanding about various businesses. In a few years he was joined by his brother Shri Tilokchandji Himatmalji Kothari and both started a Adhat Pedhi in the name of Tilokchand Rajkamal Adat. The business started flourishing and Shri Vastimal Tilokchandji Kothari also joined this family pedi business. Thus the foundation was firmly laid for other ventures to come. Shri Balchandji Kothari, son of Shri Vastimalji Kothari joined the family adat business. In 1981 he started the textile trading company specializing in uniform fabrics. In early 90’s Shri Balchandji Kothari launched the school uniform fabrics manufacturing unit. Since then there has been no looking back, and today Darshan Valji Uniforms is amongst the largest and one of the most respected uniform manufacturing and exporting company of India.
"Our fibres can be used in their 100% form, or be blended with all natural and synthetic fibres for enhanced comfort, feel and lustre. Over the years, our fibres have found new and path-breaking innovations to add comfort to your life."
Our skin-friendly fabrics are extremely popular in the trade because of their softness and feel which is a must for the little toddlers in uniforms whose parents do not want any irritation on the sensitive skins of their child.
Our school uniform fabrics are highly demanded for their distinct shades, colors as per the quality norms. The uniform fabrics are checked on various defined parameters in order to face the stringent industry standards.
We are regarded as one of the most renowned manufacturer for all types of corporate wear. With the aid of our large production and excellent storage facility, we have been able to manage bulk demands in the most efficient manner.
Our Industrial uniform fabrics are well known for their durability because once stitched the uniform gets exposed to harsh and tough work environment. To ensure this the fabrics goes stringent quality checks at all stages of production.
"We believe that Fashion is a language that creates itself in clothes to interpret reality."
"Variety's the very spice of life, that gives it all it's flavour."
"The most complicated skill is to be simple."
"When the trust account is high, communication is easy, instant, and effective."


CHANGELOG¶
1.1.2¶
more fixes for create_new flag tests
1.1.1¶
fixing tests for create_new flag
1.1.0¶
DSS file only created when explicitly create_new=True(default: False)
1.0.2¶
bugfix for empty arrays
1.0.1¶
handle pandas Series on writes
1.0.0¶
using generators for get_ts and get_matching_ts functions for efficiency context manager for use “with” statement fixed for pandas >=1.1 auto versioning turned on
0.6.1¶
fixed bug when switching to non-condensed catalog that caused shortening of time windows
0.6.0¶
fix for breaking change by pandas >= 1.1
switching to using non-condensed catalog, flag available to switch back
changing exception on missing pathname to logging message
changing message level to 0 as default
adding get_rts_matching for pathname selection by regular expressions
replaced warnings with debug logging
0.5.1¶
Fixed for ‘*’ in catalog file in case of missing periods
0.5.0¶
Added helper function for simple timeseries retrieval
0.4.1¶
regular and irregular timeseries now share same time window parsing logic
0.4.0¶
fixes for issue #16: pandas timestamp limitations
0.3.1¶
another fix for pandas 1.0.0 upgrade - issue #15
0.3.0¶
fix for issue 15: units ‘M’ and ‘Y’ no longer supported
0.2.9¶
Fixed issue with end of timestamp writing to dss files for “PER-*” data type
0.2.8¶
Recompiled heclib in linux with latest compilers to resolve issue 8
0.2.7¶
Partial fixes for offset: Fixed for INST-* timeseries but not PER-* timeseries (issue #12)
0.2.6¶
Performance tests added to showcase pyhecdss is the fastest Fixed issue #10: Period data stored shifted to end of time stamp (HEC-DSS convention) Fixing libgfortran dependency on linux by statically linking the library
0.2.5¶
Merged pull request from HenryDane: issues warnings or throws exception based on return value from functions fixed minor typo(s), added tests
0.2.4¶
Fixes issues #2, #4: get_version(), set_message_level(), set_program_name() now supported at module level Fixes issues #1: HECDSS marks periods by end of time stamp bug
0.2.3¶
Added linux 64bit support Corrected license to MIT for conda distribution
0.2.2¶
Update tests to use a smaller test.dss files Added sphinx documentation and demo notebook
0.2.1¶
Write irregular time series
0.2.0¶
Write regular time series Read irregular time series as data frame + units + type Performance improvement to using np.zeros instead of np.array(range…)


:: com :: sun :: star :: ui ::
|
| interface XUIElementFactory |
|
- Description
- specifies a user interface element factory that can create and initialize
user interface elements.
User interface element factories must be registered at a
UIElementFactoryManager service to provide access to itself.
Currently the following user interface element types are defined:
- menubarA configurable user interface element.
- popupmenuA configurable user interface element.
- toolbarA configurable user interface element.
- statusbarA configurable user interface element.
- floaterA basic user interface element.
- Since
- OOo 2.0
|
| Methods' Summary |
| createUIElement |
creates a new instances of a specific user interface element.
|
| Methods' Details |
createUIElement
- Description
- creates a new instances of a specific user interface element.
- Parameter ResourceURL
- specifies which unique user interface element should be created
by the factory. A resourcce URL must meet the following syntax:
"private:resource/$type/$name. It is only allowed to use ascii
characters for type and name. This argument must not be empty to
have a working user interface element instance.The implementation
can throw an
::com::sun::star::container::NoSuchElementException
if it doesn't know how to create the request user interface
element.
- Parameter Args
- The following arguments are supported:
- Frame
specifies the ::com::sun::star::frame::XFrame
instance to which the user interface element belongs to. To
create a configurable user interface element the frame
instance must contain a visible component. Otherwise it is
not possible to determine the correct user interface
configuration manager. This argument is mandatory to
have a working configurable user interface element instance.
- ParentWindow
specifies a parent window to use for the window(s) representing
the UI element. Depending on the concrete UI element type, this parameter
might be required or ignored by an implementation.
- Persistent
specifies if changes to a configurable
user interface element should be persistent. This is an
optional argument. The default value is true.
An implementation is responsible to initialize every newly created user
interface element if the necessary properties are provided. Especially
it must connect a configurable user interface element to the correct user
interface configuration manager. Without this connection the configurable
user interface element cannot retrieve its structure data and changes to
the user interface element structure won't be persistent. It is up to the
implementation to throw an
::com::sun::star::lang::IllegalArgumentException
if it cannot create a user interface element with the provided arguments.
- See also
- ConfigurableUIElement
- See also
- UIElement
|
|
Top of Page
Copyright © 2013, The Apache Software Foundation, Licensed under the Apache License, Version 2.0. Apache, the Apache feather logo, Apache OpenOffice and OpenOffice.org are trademarks of The Apache Software Foundation. Other names may be trademarks of their respective owners.


We monetize mices!
- seize clicks-and-mortar paradigms
- synergize interactive infomediaries
- incubate value-added metrics
- envisioneer user-centric eyeballs
- cultivate cutting-edge models
- architect B2C e-services
- enhance integrated niches
- expedite holistic methodologies
- expedite virtual initiatives
- revolutionize revolutionary web-readiness
- facilitate bleeding-edge markets


View national funding formula for your school: 2020 to 2021
Find out how much funding is allocated for your school using the national funding formula.
You can view funding for these mainstream schools:
- schools maintained by a local authority
- academies
- free schools
The funding covers 5 to 16 year olds.


PLIPCONFIG
Section: (8)Updated: 17 February 1995
Index Return to Main Contents
NAME
plipconfig - fine tune PLIP device parametersSYNOPSIS
plipconfig interface [nibble NN] [trigger NN]plipconfig [-V] [--version] [-h] [--help]
DESCRIPTION
Plipconfig is used to (hopefully) improve PLIP performance by changing the default timing parameters used by the PLIP protocol. Results are dependent on the parallel port hardware, cable, and the CPU speed of each machine on each end of the PLIP link.If the single interface argument is given, plipconfig displays the status of the given interface only. Otherwise, it will try to set the options.
OPTIONS
- nibble NN
- Sets the nibble wait value in microseconds. Default is 3000.
- trigger NN
- Sets the trigger wait value in microseconds. Default is 500.
PLIP speed can in some cases be improved by lowering the default values. Values which are too low may cause excess use of CPU, poor interrupt response time resulting in serial ports dropping characters, or in dropping of PLIP packets. Changing the plip MTU can also affect PLIP speed.
NOTE
If you get no response it is far more likely the irq is wrong and needs setting with ifconfig. The few cases where the default parameters will be too fast are those using very long cables. Something you should never do as the parallel port is not specified or designed for driving long cable runs.SEE ALSO
ifconfig(8)BUGS
Non.AUTHOR
John Paul Morrison<EMAIL_ADDRESS><EMAIL_ADDRESS>Index
This document was created by man2html, using the manual pages.
Time: 05:34:28 GMT, December 24, 2015


Could someone survive inside a transporter buffer for 75 years? Wouldn't that bring about chaos? And blowing into maximum warp speed, you appeared for an instant to be in two places at once. For an android with no feelings, he sure managed to evoke them in others.
Is it my imagination, or have tempers become a little frayed on the ship lately? When has justice ever been as simple as a rule book? Yes, absolutely, I do indeed concur, wholeheartedly! The look in your eyes, I recognize it. You used to have it for me.
Is it my imagination, or have tempers become a little frayed on the ship lately? When has justice ever been as simple as a rule book? Yes, absolutely, I do indeed concur, wholeheartedly! The look in your eyes, I recognize it. You used to have it for me.


Home
About Us
Members
Documents
Meeting Notes
Tasks
Issue Committees
Food
GPA
Uniform
Bathroom
Contact
Contact
Us
Email Us
Facebook
Form
Suggestion Box
Copyright 2015-2016 ISB Student Council. Made by
Daiki
and the
Software Development Club.


For any Registration related queries, contact: Vinit : +91-8239581631 Vandita : +91-9928086307 Shashvat Tripathi : +91-7728807727
Department of Publications and Participation : pcr@bits-oasis.org


This tool aims to provide translation to Umamusume ingame text by patching text_data
table in master.mdb
file.
This process is done completely in the browser. To contribute or get more details, please check the GitHub Repository.
master.mdb
file after clicking the button belowC:\Users\YourUsername\AppData\LocalLow\Cygames\umamusume\master\master.mdb
master.mdb
file with the translated master.mdb
filemaster.mdb
, so this method does not fully translate the game; e.g. story text remains intact.master.mdb
is replaced, you will need to redo the process.master.mdb
in mobile devices, it's just more painful to do.


M.
blog
contact
about
Hi, I'm Madhav
I make apps, websites and UI that modern trends demand.
Contact Me


order confirmation
Thank you for your purchase!
A confirmation email has been sent to<EMAIL_ADDRESS>Order No:458665214032
Order Status: Pending
Return to Home
Copyright © 2020 Shoppy Bazar. All Copyright Reserved | Privacy Policy
Template By: Arijit Saha Ray