feat(frontends/lean): add compact notation for setting attributes suggested by Sebastian
This commit is contained in:
Leonardo de Moura
parent
d1653abe57
commit
49cffc0b20
12 changed files with 67 additions and 94 deletions
|
|
@ -52,14 +52,6 @@ inductive sum (A : Type u) (B : Type v)
|
|||
| inl {} : A → sum
|
||||
| inr {} : B → sum
|
||||
|
||||
attribute [reducible]
|
||||
def sum.intro_left {A : Type u} (B : Type v) (a : A) : sum A B :=
|
||||
sum.inl a
|
||||
|
||||
attribute [reducible]
|
||||
def sum.intro_right (A : Type u) {B : Type v} (b : B) : sum A B :=
|
||||
sum.inr b
|
||||
|
||||
inductive or (a b : Prop) : Prop
|
||||
| inl {} : a → or
|
||||
| inr {} : b → or
|
||||
|
|
|
|||
|
|
@ -11,12 +11,10 @@ notation f ` $ `:1 a:1 := f a
|
|||
universe variables u_a u_b u_c u_d u_e
|
||||
variables {A : Type u_a} {B : Type u_b} {C : Type u_c} {D : Type u_d} {E : Type u_a}
|
||||
|
||||
attribute [inline, reducible]
|
||||
def function.comp (f : B → C) (g : A → B) : A → C :=
|
||||
@[inline, reducible] def function.comp (f : B → C) (g : A → B) : A → C :=
|
||||
λ x, f (g x)
|
||||
|
||||
attribute [inline, reducible]
|
||||
def function.dcomp {B : A → Type u_b} {C : Π {x : A}, B x → Type u_c}
|
||||
@[inline, reducible] def function.dcomp {B : A → Type u_b} {C : Π {x : A}, B x → Type u_c}
|
||||
(f : Π {x : A} (y : B x), C y) (g : Π x, B x) : Π x, C (g x) :=
|
||||
λ x, f (g x)
|
||||
|
||||
|
|
@ -25,41 +23,32 @@ infixr ` ∘' `:80 := function.dcomp
|
|||
|
||||
namespace function
|
||||
|
||||
attribute [reducible]
|
||||
def comp_right (f : B → B → B) (g : A → B) : B → A → B :=
|
||||
@[reducible] def comp_right (f : B → B → B) (g : A → B) : B → A → B :=
|
||||
λ b a, f b (g a)
|
||||
|
||||
attribute [reducible]
|
||||
def comp_left (f : B → B → B) (g : A → B) : A → B → B :=
|
||||
@[reducible] def comp_left (f : B → B → B) (g : A → B) : A → B → B :=
|
||||
λ a b, f (g a) b
|
||||
|
||||
attribute [reducible]
|
||||
def on_fun (f : B → B → C) (g : A → B) : A → A → C :=
|
||||
@[reducible] def on_fun (f : B → B → C) (g : A → B) : A → A → C :=
|
||||
λ x y, f (g x) (g y)
|
||||
|
||||
attribute [reducible]
|
||||
def combine (f : A → B → C) (op : C → D → E) (g : A → B → D)
|
||||
@[reducible] def combine (f : A → B → C) (op : C → D → E) (g : A → B → D)
|
||||
: A → B → E :=
|
||||
λ x y, op (f x y) (g x y)
|
||||
|
||||
attribute [reducible]
|
||||
def const (B : Type u_b) (a : A) : B → A :=
|
||||
@[reducible] def const (B : Type u_b) (a : A) : B → A :=
|
||||
λ x, a
|
||||
|
||||
attribute [reducible]
|
||||
def swap {C : A → B → Type u_c} (f : Π x y, C x y) : Π y x, C x y :=
|
||||
@[reducible] def swap {C : A → B → Type u_c} (f : Π x y, C x y) : Π y x, C x y :=
|
||||
λ y x, f x y
|
||||
|
||||
attribute [reducible]
|
||||
def app {B : A → Type u_b} (f : Π x, B x) (x : A) : B x :=
|
||||
@[reducible] def app {B : A → Type u_b} (f : Π x, B x) (x : A) : B x :=
|
||||
f x
|
||||
|
||||
attribute [reducible]
|
||||
def curry : (A × B → C) → A → B → C :=
|
||||
@[reducible] def curry : (A × B → C) → A → B → C :=
|
||||
λ f a b, f (a, b)
|
||||
|
||||
attribute [reducible]
|
||||
def uncurry : (A → B → C) → (A × B → C) :=
|
||||
@[reducible] def uncurry : (A → B → C) → (A × B → C) :=
|
||||
λ f p, match p with (a, b) := f a b end
|
||||
|
||||
theorem curry_uncurry (f : A → B → C) : curry (uncurry f) = f :=
|
||||
|
|
@ -83,15 +72,13 @@ theorem comp.right_id (f : A → B) : f ∘ id = f := rfl
|
|||
|
||||
theorem comp_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) := rfl
|
||||
|
||||
attribute [reducible]
|
||||
def injective (f : A → B) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
|
||||
@[reducible] def injective (f : A → B) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
|
||||
|
||||
theorem injective_comp {g : B → C} {f : A → B} (Hg : injective g) (Hf : injective f) :
|
||||
injective (g ∘ f) :=
|
||||
take a₁ a₂, assume Heq, Hf (Hg Heq)
|
||||
|
||||
attribute [reducible]
|
||||
def surjective (f : A → B) : Prop := ∀ b, ∃ a, f a = b
|
||||
@[reducible] def surjective (f : A → B) : Prop := ∀ b, ∃ a, f a = b
|
||||
|
||||
theorem surjective_comp {g : B → C} {f : A → B} (Hg : surjective g) (Hf : surjective f) :
|
||||
surjective (g ∘ f) :=
|
||||
|
|
|
|||
|
|
@ -8,8 +8,7 @@ import init.datatypes
|
|||
|
||||
universe variables u v w
|
||||
|
||||
attribute [reducible]
|
||||
def id {A : Type u} (a : A) : A := a
|
||||
@[reducible] def id {A : Type u} (a : A) : A := a
|
||||
|
||||
def flip {A : Type u} {B : Type v} {C : Type w} (f : A → B → C) : B → A → C :=
|
||||
λ b a, f a b
|
||||
|
|
@ -18,8 +17,7 @@ def flip {A : Type u} {B : Type v} {C : Type w} (f : A → B → C) : B → A
|
|||
|
||||
def implies (a b : Prop) := a → b
|
||||
|
||||
attribute [trans]
|
||||
lemma implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
|
||||
@[trans] lemma implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
|
||||
assume hp, h₂ (h₁ hp)
|
||||
|
||||
def trivial : true := ⟨⟩
|
||||
|
|
@ -27,8 +25,7 @@ def trivial : true := ⟨⟩
|
|||
def not (a : Prop) := a → false
|
||||
prefix `¬` := not
|
||||
|
||||
attribute [inline]
|
||||
def absurd {a : Prop} {b : Type v} (h₁ : a) (h₂ : ¬a) : b :=
|
||||
@[inline] def absurd {a : Prop} {b : Type v} (h₁ : a) (h₂ : ¬a) : b :=
|
||||
false.rec b (h₂ h₁)
|
||||
|
||||
lemma not.intro {a : Prop} (h : a → false) : ¬ a :=
|
||||
|
|
@ -60,8 +57,7 @@ false.rec c h
|
|||
lemma proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ :=
|
||||
rfl
|
||||
|
||||
attribute [defeq]
|
||||
def id.def {A : Type u} (a : A) : id a = a := rfl
|
||||
@[defeq] def id.def {A : Type u} (a : A) : id a = a := rfl
|
||||
|
||||
-- Remark: we provide the universe levels explicitly to make sure `eq.drec` has the same type of `eq.rec` in the hoTT library
|
||||
attribute [elab_as_eliminator]
|
||||
|
|
@ -117,8 +113,7 @@ section
|
|||
assume hp, h ▸ hp
|
||||
end
|
||||
|
||||
attribute [inline]
|
||||
def cast {A B : Type u} (h : A = B) (a : A) : B :=
|
||||
@[inline] def cast {A B : Type u} (h : A = B) (a : A) : B :=
|
||||
eq.rec a h
|
||||
|
||||
lemma cast_proof_irrel {A B : Type u} (h₁ h₂ : A = B) (a : A) : cast h₁ a = cast h₂ a :=
|
||||
|
|
@ -129,10 +124,9 @@ rfl
|
|||
|
||||
/- ne -/
|
||||
|
||||
attribute [reducible]
|
||||
def ne {A : Type u} (a b : A) := ¬(a = b)
|
||||
attribute [defeq]
|
||||
def ne.def {A : Type u} (a b : A) : ne a b = ¬ (a = b) := rfl
|
||||
@[reducible] def ne {A : Type u} (a b : A) := ¬(a = b)
|
||||
|
||||
@[defeq] def ne.def {A : Type u} (a b : A) : ne a b = ¬ (a = b) := rfl
|
||||
notation a ≠ b := ne a b
|
||||
|
||||
namespace ne
|
||||
|
|
@ -638,14 +632,12 @@ is_false not_false
|
|||
|
||||
-- We use "dependent" if-then-else to be able to communicate the if-then-else condition
|
||||
-- to the branches
|
||||
attribute [inline]
|
||||
def dite (c : Prop) [h : decidable c] {A : Type u} : (c → A) → (¬ c → A) → A :=
|
||||
@[inline] def dite (c : Prop) [h : decidable c] {A : Type u} : (c → A) → (¬ c → A) → A :=
|
||||
λ t e, decidable.rec_on h e t
|
||||
|
||||
/- if-then-else -/
|
||||
|
||||
attribute [inline]
|
||||
def ite (c : Prop) [h : decidable c] {A : Type u} (t e : A) : A :=
|
||||
@[inline] def ite (c : Prop) [h : decidable c] {A : Type u} (t e : A) : A :=
|
||||
decidable.rec_on h (λ hnc, e) (λ hc, t)
|
||||
|
||||
namespace decidable
|
||||
|
|
@ -713,12 +705,9 @@ section
|
|||
and.decidable
|
||||
end
|
||||
|
||||
attribute [reducible]
|
||||
def decidable_pred {A : Type u} (r : A → Prop) := Π (a : A), decidable (r a)
|
||||
attribute [reducible]
|
||||
def decidable_rel {A : Type u} (r : A → A → Prop) := Π (a b : A), decidable (r a b)
|
||||
attribute [reducible]
|
||||
def decidable_eq (A : Type u) := decidable_rel (@eq A)
|
||||
@[reducible] def decidable_pred {A : Type u} (r : A → Prop) := Π (a : A), decidable (r a)
|
||||
@[reducible] def decidable_rel {A : Type u} (r : A → A → Prop) := Π (a b : A), decidable (r a b)
|
||||
@[reducible] def decidable_eq (A : Type u) := decidable_rel (@eq A)
|
||||
|
||||
instance {A : Type u} [decidable_eq A] (a b : A) : decidable (a ≠ b) :=
|
||||
implies.decidable
|
||||
|
|
@ -762,8 +751,7 @@ class inhabited (A : Type u) :=
|
|||
def default (A : Type u) [inhabited A] : A :=
|
||||
inhabited.default A
|
||||
|
||||
attribute [inline, irreducible]
|
||||
def arbitrary (A : Type u) [inhabited A] : A :=
|
||||
@[inline, irreducible] def arbitrary (A : Type u) [inhabited A] : A :=
|
||||
default A
|
||||
|
||||
instance prop.inhabited : inhabited Prop :=
|
||||
|
|
|
|||
|
|
@ -92,8 +92,7 @@ namespace nat
|
|||
protected definition le_refl : ∀ a : ℕ, a ≤ a :=
|
||||
le.nat_refl
|
||||
|
||||
attribute [reducible]
|
||||
protected definition lt (n m : ℕ) := succ n ≤ m
|
||||
@[reducible] protected definition lt (n m : ℕ) := succ n ≤ m
|
||||
|
||||
instance : has_lt ℕ :=
|
||||
⟨nat.lt⟩
|
||||
|
|
|
|||
|
|
@ -128,6 +128,8 @@
|
|||
`((;; attributes
|
||||
(,(rx word-start "attribute" word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace))))
|
||||
(1 'font-lock-doc-face))
|
||||
(,(rx (group "@[" (zero-or-more (not (any "]"))) "]"))
|
||||
(1 'font-lock-doc-face))
|
||||
;; mutal definitions "names"
|
||||
(,(rx word-start
|
||||
"mutual"
|
||||
|
|
|
|||
|
|
@ -15,10 +15,7 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/util.h"
|
||||
|
||||
namespace lean {
|
||||
void decl_attributes::parse(parser & p) {
|
||||
if (!p.curr_is_token(get_lbracket_tk()))
|
||||
return;
|
||||
p.next();
|
||||
void decl_attributes::parse_core(parser & p, bool compact) {
|
||||
while (true) {
|
||||
auto pos = p.pos();
|
||||
bool deleted = p.curr_is_token_or_id(get_sub_tk());
|
||||
|
|
@ -73,6 +70,8 @@ void decl_attributes::parse(parser & p) {
|
|||
p.next();
|
||||
} else {
|
||||
p.check_token_next(get_rbracket_tk(), "invalid attribute declaration, ']' expected");
|
||||
if (compact)
|
||||
break;
|
||||
if (p.curr_is_token(get_lbracket_tk()))
|
||||
p.next();
|
||||
else
|
||||
|
|
@ -81,6 +80,17 @@ void decl_attributes::parse(parser & p) {
|
|||
}
|
||||
}
|
||||
|
||||
void decl_attributes::parse(parser & p) {
|
||||
if (!p.curr_is_token(get_lbracket_tk()))
|
||||
return;
|
||||
p.next();
|
||||
parse_core(p, false);
|
||||
}
|
||||
|
||||
void decl_attributes::parse_compact(parser & p) {
|
||||
parse_core(p, true);
|
||||
}
|
||||
|
||||
void decl_attributes::set_attribute(environment const & env, name const & attr_name) {
|
||||
if (!is_attribute(env, attr_name))
|
||||
throw exception(sstream() << "unknown attribute [" << attr_name << "]");
|
||||
|
|
|
|||
|
|
@ -23,10 +23,14 @@ private:
|
|||
bool m_parsing_only;
|
||||
list<entry> m_entries;
|
||||
optional<unsigned> m_prio;
|
||||
void parse_core(parser & p, bool compact);
|
||||
public:
|
||||
decl_attributes(bool persistent = true): m_persistent(persistent), m_parsing_only(false) {}
|
||||
void set_attribute(environment const & env, name const & attr_name);
|
||||
/* attributes: zero-or-more [ ... ] */
|
||||
void parse(parser & p);
|
||||
/* Parse attributes after `@[` ... ] */
|
||||
void parse_compact(parser & p);
|
||||
environment apply(environment env, io_state const & ios, name const & d) const;
|
||||
list<entry> const & get_entries() const { return m_entries; }
|
||||
bool is_parsing_only() const { return m_parsing_only; }
|
||||
|
|
|
|||
|
|
@ -527,6 +527,19 @@ environment local_attribute_cmd(parser & p) {
|
|||
return attribute_cmd_core(p, false);
|
||||
}
|
||||
|
||||
static environment compact_attribute_cmd(parser & p) {
|
||||
bool persistent = true;
|
||||
decl_attributes attributes(persistent);
|
||||
attributes.parse_compact(p);
|
||||
if (p.curr_is_token_or_id(get_inductive_tk())) {
|
||||
return inductive_cmd_ex(p, attributes);
|
||||
} else if (p.curr_is_token_or_id(get_structure_tk())) {
|
||||
return structure_cmd_ex(p, attributes, false);
|
||||
} else {
|
||||
return definition_cmd_ex(p, attributes);
|
||||
}
|
||||
}
|
||||
|
||||
static environment include_cmd_core(parser & p, bool include) {
|
||||
if (!p.curr_is_identifier())
|
||||
throw parser_error(sstream() << "invalid include/omit command, identifier expected", p.pos());
|
||||
|
|
@ -591,6 +604,7 @@ void register_decl_cmds(cmd_table & r) {
|
|||
add_cmd(r, cmd_info("reveal", "reveal given theorems", reveal_cmd));
|
||||
add_cmd(r, cmd_info("include", "force section parameter/variable to be included", include_cmd));
|
||||
add_cmd(r, cmd_info("attribute", "set declaration attributes", attribute_cmd));
|
||||
add_cmd(r, cmd_info("@[", "declaration attributes", compact_attribute_cmd));
|
||||
add_cmd(r, cmd_info("omit", "undo 'include' command", omit_cmd));
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -100,20 +100,15 @@ void init_token_table(token_table & t) {
|
|||
|
||||
char const * commands[] =
|
||||
{"theorem", "axiom", "axioms", "variable", "protected", "private", "reveal",
|
||||
"definition", "meta", "mutual",
|
||||
"example", "coercion", "noncomputable",
|
||||
"definition", "meta", "mutual", "example", "coercion", "noncomputable",
|
||||
"variables", "parameter", "parameters", "constant", "constants",
|
||||
"[visible]", "[none]",
|
||||
"evaluate", "check", "eval", "vm_eval", "using_well_founded", "[whnf]", "[unfold_hints]",
|
||||
"evaluate", "check", "eval", "vm_eval", "using_well_founded", "[whnf]",
|
||||
"print", "end", "namespace", "section", "prelude", "help",
|
||||
"import", "inductive", "record", "structure", "class", "universe", "universes", "local",
|
||||
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
|
||||
"tactic_infixl", "tactic_infixr", "tactic_infix", "tactic_postfix", "tactic_prefix", "tactic_notation",
|
||||
"exit", "set_option", "open", "export", "override", "tactic_hint",
|
||||
"add_begin_end_tactic", "set_begin_end_tactic",
|
||||
"multiple_instances", "find_decl", "attribute", "persistent", "instance",
|
||||
"include", "omit", "migrate",
|
||||
"init_quotient", "init_hits", "declare_trace", "register_simp_ext",
|
||||
"exit", "set_option", "open", "export", "override", "@[",
|
||||
"attribute", "persistent", "instance", "include", "omit", "init_quotient",
|
||||
"init_hits", "declare_trace", "register_simp_ext",
|
||||
"run_command", "add_key_equivalence", "#erase_cache",
|
||||
"#compile", "#unify", nullptr};
|
||||
|
||||
|
|
|
|||
|
|
@ -19,8 +19,6 @@ static name const * g_lcurly_tk = nullptr;
|
|||
static name const * g_rcurly_tk = nullptr;
|
||||
static name const * g_ldcurly_tk = nullptr;
|
||||
static name const * g_rdcurly_tk = nullptr;
|
||||
static name const * g_lcurlybar_tk = nullptr;
|
||||
static name const * g_rcurlybar_tk = nullptr;
|
||||
static name const * g_lbracket_tk = nullptr;
|
||||
static name const * g_rbracket_tk = nullptr;
|
||||
static name const * g_langle_tk = nullptr;
|
||||
|
|
@ -69,7 +67,6 @@ static name const * g_renaming_tk = nullptr;
|
|||
static name const * g_replacing_tk = nullptr;
|
||||
static name const * g_extends_tk = nullptr;
|
||||
static name const * g_as_tk = nullptr;
|
||||
static name const * g_none_tk = nullptr;
|
||||
static name const * g_whnf_tk = nullptr;
|
||||
static name const * g_in_tk = nullptr;
|
||||
static name const * g_assign_tk = nullptr;
|
||||
|
|
@ -138,8 +135,6 @@ void initialize_tokens() {
|
|||
g_rcurly_tk = new name{"}"};
|
||||
g_ldcurly_tk = new name{"⦃"};
|
||||
g_rdcurly_tk = new name{"⦄"};
|
||||
g_lcurlybar_tk = new name{"{|"};
|
||||
g_rcurlybar_tk = new name{"|}"};
|
||||
g_lbracket_tk = new name{"["};
|
||||
g_rbracket_tk = new name{"]"};
|
||||
g_langle_tk = new name{"⟨"};
|
||||
|
|
@ -188,7 +183,6 @@ void initialize_tokens() {
|
|||
g_replacing_tk = new name{"replacing"};
|
||||
g_extends_tk = new name{"extends"};
|
||||
g_as_tk = new name{"as"};
|
||||
g_none_tk = new name{"[none]"};
|
||||
g_whnf_tk = new name{"[whnf]"};
|
||||
g_in_tk = new name{"in"};
|
||||
g_assign_tk = new name{":="};
|
||||
|
|
@ -258,8 +252,6 @@ void finalize_tokens() {
|
|||
delete g_rcurly_tk;
|
||||
delete g_ldcurly_tk;
|
||||
delete g_rdcurly_tk;
|
||||
delete g_lcurlybar_tk;
|
||||
delete g_rcurlybar_tk;
|
||||
delete g_lbracket_tk;
|
||||
delete g_rbracket_tk;
|
||||
delete g_langle_tk;
|
||||
|
|
@ -308,7 +300,6 @@ void finalize_tokens() {
|
|||
delete g_replacing_tk;
|
||||
delete g_extends_tk;
|
||||
delete g_as_tk;
|
||||
delete g_none_tk;
|
||||
delete g_whnf_tk;
|
||||
delete g_in_tk;
|
||||
delete g_assign_tk;
|
||||
|
|
@ -377,8 +368,6 @@ name const & get_lcurly_tk() { return *g_lcurly_tk; }
|
|||
name const & get_rcurly_tk() { return *g_rcurly_tk; }
|
||||
name const & get_ldcurly_tk() { return *g_ldcurly_tk; }
|
||||
name const & get_rdcurly_tk() { return *g_rdcurly_tk; }
|
||||
name const & get_lcurlybar_tk() { return *g_lcurlybar_tk; }
|
||||
name const & get_rcurlybar_tk() { return *g_rcurlybar_tk; }
|
||||
name const & get_lbracket_tk() { return *g_lbracket_tk; }
|
||||
name const & get_rbracket_tk() { return *g_rbracket_tk; }
|
||||
name const & get_langle_tk() { return *g_langle_tk; }
|
||||
|
|
@ -427,7 +416,6 @@ name const & get_renaming_tk() { return *g_renaming_tk; }
|
|||
name const & get_replacing_tk() { return *g_replacing_tk; }
|
||||
name const & get_extends_tk() { return *g_extends_tk; }
|
||||
name const & get_as_tk() { return *g_as_tk; }
|
||||
name const & get_none_tk() { return *g_none_tk; }
|
||||
name const & get_whnf_tk() { return *g_whnf_tk; }
|
||||
name const & get_in_tk() { return *g_in_tk; }
|
||||
name const & get_assign_tk() { return *g_assign_tk; }
|
||||
|
|
|
|||
|
|
@ -21,8 +21,6 @@ name const & get_lcurly_tk();
|
|||
name const & get_rcurly_tk();
|
||||
name const & get_ldcurly_tk();
|
||||
name const & get_rdcurly_tk();
|
||||
name const & get_lcurlybar_tk();
|
||||
name const & get_rcurlybar_tk();
|
||||
name const & get_lbracket_tk();
|
||||
name const & get_rbracket_tk();
|
||||
name const & get_langle_tk();
|
||||
|
|
@ -71,7 +69,6 @@ name const & get_renaming_tk();
|
|||
name const & get_replacing_tk();
|
||||
name const & get_extends_tk();
|
||||
name const & get_as_tk();
|
||||
name const & get_none_tk();
|
||||
name const & get_whnf_tk();
|
||||
name const & get_in_tk();
|
||||
name const & get_assign_tk();
|
||||
|
|
|
|||
|
|
@ -14,8 +14,6 @@ lcurly {
|
|||
rcurly }
|
||||
ldcurly ⦃
|
||||
rdcurly ⦄
|
||||
lcurlybar {|
|
||||
rcurlybar |}
|
||||
lbracket [
|
||||
rbracket ]
|
||||
langle ⟨
|
||||
|
|
@ -64,7 +62,6 @@ renaming renaming
|
|||
replacing replacing
|
||||
extends extends
|
||||
as as
|
||||
none [none]
|
||||
whnf [whnf]
|
||||
in in
|
||||
assign :=
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue