Functions — github.com/ammkrn/nanoda

hub / github.com/ammkrn/nanoda / functions

Functions297 in github.com/ammkrn/nanoda

The "heights" of two terms `E1` and `E2` are used to determine whether one is defined in terms of or uses terms derived from the other. If at some poi

src/tc.rs:64

↓ 2 callersMethoddist_to_first_line

(&self)

src/pretty/components.rs:167

↓ 2 callersMethoddist_to_line

(&self, after : usize)

src/pretty/components.rs:177

↓ 2 callersMethodensure_imax_leq

This is used in `leq_core` to handle the case where one of the levels in question is an IMax whose right hand side is some paramter `P`. In light of t

src/level.rs:154

↓ 2 callersFunctionfind_first_usize

(s : &str)

src/cli.rs:87

↓ 2 callersMethodfresh_name

(&self, suggestion : &Name)

src/pretty/pretty_printer.rs:108

↓ 2 callersMethodget_name

(&self)

src/inductive.rs:113

↓ 2 callersMethodget_uparams

(&mut self, ws : &mut SplitWhitespace)

src/parser.rs:154

↓ 2 callersMethodget_ups

(&self, declar : &Declaration)

src/pretty/pretty_printer.rs:371

↓ 2 callersMethodindep_declaration_check

(&self, env : Arc<RwLock<Env>>)

src/env.rs:118

↓ 2 callersMethodinstantiate_ps

This just performs variable substitution by going through the `Level` items contained in `Sort` and `Const` expressions. For all levels therein, attem

src/expr.rs:402

↓ 2 callersMethodis_any_max

(&self)

src/level.rs:73

↓ 2 callersMethodis_imp

(&self)

src/pretty/pretty_printer.rs:533

↓ 2 callersMethodis_proposition

tries is_prop after inferring e

src/tc.rs:85

↓ 2 callersMethodleq

Outward-facing function that uses `leq_core` to determine whether for two levels `L1` and `L2`, `L1 <= L2` using Lean's definition of order on univers

src/level.rs:242

↓ 2 callersFunctionloop_add

Constantly poll the `add_queue` to see if there's something to add. If the item popped off the queue is a Left(Mod), add said mod. `None` means there

src/main.rs:173

↓ 2 callersMethodmaybe_nonzero

(&self)

src/level.rs:280

↓ 2 callersMethodnum_declars

(&self)

src/env.rs:210

↓ 2 callersMethodparse_binder_info

(&mut self, ws : &mut SplitWhitespace)

src/parser.rs:164

↓ 2 callersMethodparse_u64

(&mut self, ws : &mut SplitWhitespace)

src/parser.rs:131

↓ 2 callersFunctionpp_bundle

Just prints to stdout until I figure out what I actually want to do with this.

src/cli.rs:152

↓ 2 callersMethodprint_default

(&self, f : &Expr, apps : &Vec<Expr>)

src/pretty/pretty_printer.rs:282

↓ 2 callersMethodref_prop

(&self)

src/parser.rs:75

↓ 2 callersMethodref_zero

(&self)

src/parser.rs:71

↓ 2 callersMethodrequire_def_eq

(&mut self, e1 : &Expr, e2 : &Expr)

src/tc.rs:669

↓ 2 callersMethodto_offset

(&self)

src/level.rs:284

↓ 2 callersFunctionunique_univ_params

(lvl : &'l Level)

src/level.rs:297

↓ 1 callersMethodabstract_core

(&self, offset : usize, locals : impl Iterator<Item = &'e Expr> + Clone, cache : &mut OffsetCache)

src/expr.rs:291

↓ 1 callersMethodadd_notation

(&mut self, n : &Name, notation: Notation)

src/env.rs:203

↓ 1 callersMethodadd_rule

Inserting a new ReductionRule into rules, and ADDING its majors to the cumulative set of the other Name |-> Vec<ReductionRule> mapping's majors. Also

src/reduction.rs:249

↓ 1 callersMethodapply_hd_tl

(&self, hd : &Expr, apps : &[Expr], cache : &mut ReductionCache)

src/reduction.rs:183

↓ 1 callersMethodapply_lambda

Given two expressions `E` and `L`, where `L` is known to be a Local, ```pseudo let E' = E.abstract(L) return (λ L, E') ```

src/expr.rs:582

↓ 1 callersMethodapply_pi

Given two expressions `E` and `L`, where `L` is known to be a Local : ```pseudo let E = E.abstract(L) return (Π (L) (E')) ```

src/expr.rs:521

↓ 1 callersMethodapply_reduction

(&self, e : Expr, cache : &mut Reductio

src/reduction.rs:147

↓ 1 callersMethodapply_to_map

(&self, e : Expr, cache : &mut ReductionCache)

src/reduction.rs:226

↓ 1 callersMethodbinder_is_pi

!! Partial function !! only used once in the pretty printer.

src/expr.rs:227

↓ 1 callersMethodcheck_def_eq_lambdas

Literally the same function as its Pi counterpart, but checks for a different enum discriminant (Lambdas instead of Pis).

src/tc.rs:458

↓ 1 callersMethodcheck_def_eq_patterns

Dispatch point for different decision procedures used to determine whether two expressions are definitionally equal in a certain context.

src/tc.rs:341

↓ 1 callersMethodcheck_def_eq_pis

Literally the same function as its Lambda counterpart, but checks for a different enum discriminant (Pis instead of Lambdas).

src/tc.rs:409

↓ 1 callersMethodcheck_intro

check an introduction rule

src/inductive.rs:458

↓ 1 callersMethodcheck_only

Checks a given item.

src/env.rs:308

↓ 1 callersFunctioncheck_parallel

(source : String, num_threads : usize, print : bool)

src/main.rs:117

↓ 1 callersFunctioncheck_serial

(source : String, print : bool)

src/main.rs:97

↓ 1 callersMethodcollect_substs

(&self, e1 : &'l Expr, e2 : &'l Expr,

src/reduction.rs:109

↓ 1 callersMethodcombining

A non-naive way of combining two `Level` values (naive would be just creating a Max). gets used in `simplify`.

src/level.rs:82

↓ 1 callersMethodcompile

(self, env : &Arc<RwLock<Env>>)

src/env.rs:219

↓ 1 callersMethodcompile

(self, env : &Arc<RwLock<Env>>)

src/inductive.rs:167

↓ 1 callersMethodcompile_self

(self)

src/quot.rs:158

↓ 1 callersMethodconst_name

(&self, n : &Name)

src/pretty/pretty_printer.rs:226

↓ 1 callersMethodcontains_line

(&self)

src/pretty/components.rs:157

↓ 1 callersMethodelim_into_prop

(&self, compiled_intros : &Vec<CompiledIntro>)

src/inductive.rs:125

↓ 1 callersMethodelim_level

(&self, compiled_intros : &Vec<CompiledIntro>)

src/inductive.rs:137

↓ 1 callersMethodelim_level_params

(&self, elim_level : &Level)

src/inductive.rs:150

↓ 1 callersFunctionerr_add_rule

(loc : u32, name : &T)

src/errors.rs:79

↓ 1 callersFunctionerr_binding_lc

(loc : u32, owise : &T)

src/errors.rs:24

↓ 1 callersFunctionerr_check_type

(loc : u32, got1 : &T, got2 : &T)

src/errors.rs:69

↓ 1 callersFunctionerr_get_serial

(loc : u32, owise : &T)

src/errors.rs:14

↓ 1 callersFunctionerr_infer_apps

(loc : u32, got : &T)

src/errors.rs:59

↓ 1 callersFunctionerr_infer_const

(loc : u32, name : &T)

src/errors.rs:49

↓ 1 callersFunctionerr_infer_universe

(loc : u32, got : &T)

src/errors.rs:54

↓ 1 callersFunctionerr_infer_var

(loc : u32, got : &T)

src/errors.rs:44

↓ 1 callersFunctionerr_lc_binding

(loc : u32, owise : &T)

src/errors.rs:19

↓ 1 callersFunctionerr_normalize_pis

(loc : u32, got : &T)

src/errors.rs:39

↓ 1 callersFunctionerr_offset_cache

(loc : u32, idx : usize, len : usize)

src/errors.rs:34

↓ 1 callersFunctionerr_param_name

(loc : u32, got : &T)

src/errors.rs:84

↓ 1 callersFunctionerr_parse_kind

(t : &T)

src/errors.rs:112

↓ 1 callersFunctionerr_req_def_eq

(loc : u32, got1 : &T, got2 : &T)

src/errors.rs:64

↓ 1 callersFunctionerr_rr_const

(loc : u32, got : &T)

src/errors.rs:74

↓ 1 callersFunctionerr_swap_local_binding_name

(loc : u32, owise : &T)

src/errors.rs:29

↓ 1 callersMethodfind_unused

This is why Lean's pretty printer is so hard to read w/ `B_ih_1_a_1_hwf`

src/pretty/pretty_printer.rs:98

↓ 1 callersMethodflat_size

(&self)

src/pretty/components.rs:147

↓ 1 callersMethodfold_lambdas

Given a list of Local expressions [L_1, L_2, ... L_n] and a body `E : Expr`, use your favorite method (here we use a right fold) and the Lambda constr

src/expr.rs:604

↓ 1 callersMethodget_declaration_height

(&self, name : &Name)

src/env.rs:187

↓ 1 callersMethodget_levels

(&mut self, ws : &mut SplitWhitespace)

src/parser.rs:147

↓ 1 callersMethodget_major_premises

(&self, key : &Name)

src/reduction.rs:268

↓ 1 callersMethodget_param_name

(&self)

src/level.rs:59

↓ 1 callersMethodget_serial

!! Partial function !! If the expression is a Local, returns its unique identifier/serial number. Else kills the program with a fatal error.

src/expr.rs:253

↓ 1 callersMethodget_value

(&self, n : &Name)

src/env.rs:199

↓ 1 callersFunctionhas_var

(e : &Expr, i : u64)

src/pretty/pretty_printer.rs:562

↓ 1 callersMethodinfer_apps

(&mut self, term : &Expr)

src/tc.rs:589

↓ 1 callersMethodinfer_const

(&mut self, name : &Name, levels : &Arc<Vec<Level>>)

src/tc.rs:536

↓ 1 callersMethodinfer_lambda

(&mut self, mut term : &Expr)

src/tc.rs:548

↓ 1 callersMethodinfer_let

(&mut self, dom : &Binding, val : &Expr, body : &Expr)

src/tc.rs:648

↓ 1 callersMethodinfer_pi

(&mut self, mut term : &Expr)

src/tc.rs:622

↓ 1 callersMethodinstantiate_core

The way 'offset' works is that it pushes the index further left in the vec it's indexing. Or you can think of it as pushing `None` values onto the lef

src/expr.rs:358

↓ 1 callersMethodinstantiate_pis

This only gets used once in inductive. Will use &[Expr] that comes as `toplevel_params` used during formation of intro rules. I'm not really sure how

src/tc.rs:129

↓ 1 callersMethodis_anon

(&self)

src/name.rs:29

↓ 1 callersMethodis_implicit

(&self, fun : &Expr)

src/pretty/pretty_printer.rs:130

↓ 1 callersMethodis_lambda

(&self)

src/pretty/pretty_printer.rs:544

↓ 1 callersMethodis_nonzero

for any level `L`, if Succ (Zero) is less than or equal to `L`, it cannot be that L is equal to Zero ```pseudo ∀ (L : Level), S (Zero) ≤ L → L ≠ 0 ```

src/level.rs:272

↓ 1 callersMethodis_proof_irrel_eq

(&mut self, e1: &Expr, e2: &Expr)

src/tc.rs:95

↓ 1 callersMethodis_prop

e is a prop iff it destructures as Sort(Level(Zero))

src/tc.rs:77

↓ 1 callersMethodlookup_notation

(&self, name : &Name)

src/pretty/pretty_printer.rs:34

↓ 1 callersMethodmain_axiom

(&self, declar : &Declaration)

src/pretty/pretty_printer.rs:432

↓ 1 callersMethodmain_def

(&self, declar : &Declaration, val : Expr)

src/pretty/pretty_printer.rs:379

↓ 1 callersMethodmake_axiom

(&mut self, ws : &mut SplitWhitespace)

src/parser.rs:273

↓ 1 callersMethodmake_definition

(&mut self, ws : &mut SplitWhitespace)

src/parser.rs:282

↓ 1 callersMethodmake_expr

(&mut self, new_pos : usize, kind : char, ws : &mut SplitWhitespace)

src/parser.rs:217

↓ 1 callersMethodmake_inductive

(&mut self, ws : &mut SplitWhitespace)

src/parser.rs:296

↓ 1 callersMethodmake_level

(&mut self, new_pos : usize, kind : char, ws : &mut SplitWhitespace)

src/parser.rs:203

← previous next →101–200 of 297, ranked by callers