Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+ā†‘Ctrl+ā†“to navigate, Ctrl+šŸ–±ļøto focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Lean

/-!
A rudimentary export format, adapted from

with support for lean 4 kernel primitives.
-/
open Lean (HashMap HashSet)

namespace Lean

namespace Export

/- References -/
private opaque 
MethodsRefPointed: NonemptyType
MethodsRefPointed
:
NonemptyType: Type 1
NonemptyType
.{0} private def
MethodsRef: Type
MethodsRef
:
Type: Type 1
Type
:=
MethodsRefPointed: NonemptyType
MethodsRefPointed
.
type: NonemptyType ā†’ Type ?u.12
type
inductive
Entry: Sort ?u.14
Entry
|
name: Name ā†’ Entry
name
(
n: Name
n
:
Name: Type
Name
) |
level: Level ā†’ Entry
level
(n :
Level: Type
Level
) |
expr: Expr ā†’ Entry
expr
(
n: Expr
n
:
Expr: Type
Expr
) |
defn: Name ā†’ Entry
defn
(
n: Name
n
:
Name: Type
Name
) deriving
Inhabited: Sort u ā†’ Sort (max1u)
Inhabited
instance: Coe Name Entry
instance
:
Coe: semiOutParam (Sort ?u.759) ā†’ Sort ?u.758 ā†’ Sort (max(max1?u.759)?u.758)
Coe
Name: Type
Name
Entry: Type
Entry
:= āŸØ
Entry.name: Name ā†’ Entry
Entry.name
āŸ©
instance: Coe Level Entry
instance
:
Coe: semiOutParam (Sort ?u.803) ā†’ Sort ?u.802 ā†’ Sort (max(max1?u.803)?u.802)
Coe
Level: Type
Level
Entry: Type
Entry
:= āŸØ
Entry.level: Level ā†’ Entry
Entry.level
āŸ©
instance: Coe Expr Entry
instance
:
Coe: semiOutParam (Sort ?u.844) ā†’ Sort ?u.843 ā†’ Sort (max(max1?u.844)?u.843)
Coe
Expr: Type
Expr
Entry: Type
Entry
:= āŸØ
Entry.expr: Expr ā†’ Entry
Entry.expr
āŸ© structure
Alloc: {Ī± : Type u_1} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ HashMap Ī± Nat ā†’ Nat ā†’ Alloc Ī±
Alloc
(
Ī±: ?m.884
Ī±
) [
BEq: Type ?u.887 ā†’ Type ?u.887
BEq
Ī±: ?m.884
Ī±
] [
Hashable: Sort ?u.890 ā†’ Sort (max1?u.890)
Hashable
Ī±: ?m.884
Ī±
] where
map: {Ī± : Type u_1} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ Alloc Ī± ā†’ HashMap Ī± Nat
map
:
HashMap: (Ī± : Type ?u.896) ā†’ Type ?u.895 ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type (max0?u.896?u.895)
HashMap
Ī±: ?m.884
Ī±
Nat: Type
Nat
next: {Ī± : Type u_1} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ Alloc Ī± ā†’ Nat
next
:
Nat: Type
Nat
deriving
Inhabited: Sort u ā†’ Sort (max1u)
Inhabited
structure
State: Alloc Name ā†’ Alloc Level ā†’ Alloc Expr ā†’ HashSet Name ā†’ Array (Bool Ɨ Entry) ā†’ State
State
where
names: State ā†’ Alloc Name
names
:
Alloc: (Ī± : Type ?u.1773) ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type ?u.1773
Alloc
Name: Type
Name
:= āŸØ
HashMap.empty: {Ī± : Type ?u.1818} ā†’ {Ī² : Type ?u.1817} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ HashMap Ī± Ī²
HashMap.empty
.
insert: {Ī± : Type ?u.1848} ā†’ {Ī² : Type ?u.1847} ā†’ {x : BEq Ī±} ā†’ {x_1 : Hashable Ī±} ā†’ HashMap Ī± Ī² ā†’ Ī± ā†’ Ī² ā†’ HashMap Ī± Ī²
insert
Name.anonymous: Name
Name.anonymous
0: ?m.1871
0
,
1: ?m.1880
1
āŸ©
levels: State ā†’ Alloc Level
levels
:
Alloc: (Ī± : Type ?u.1886) ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type ?u.1886
Alloc
Level: Type
Level
:= āŸØ
HashMap.empty: {Ī± : Type ?u.1926} ā†’ {Ī² : Type ?u.1925} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ HashMap Ī± Ī²
HashMap.empty
.
insert: {Ī± : Type ?u.1956} ā†’ {Ī² : Type ?u.1955} ā†’ {x : BEq Ī±} ā†’ {x_1 : Hashable Ī±} ā†’ HashMap Ī± Ī² ā†’ Ī± ā†’ Ī² ā†’ HashMap Ī± Ī²
insert
levelZero: Level
levelZero
0: ?m.1975
0
,
1: ?m.1978
1
āŸ©
exprs: State ā†’ Alloc Expr
exprs
:
Alloc: (Ī± : Type ?u.1982) ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type ?u.1982
Alloc
Expr: Type
Expr
defs: State ā†’ HashSet Name
defs
:
HashSet: (Ī± : Type ?u.1990) ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type ?u.1990
HashSet
Name: Type
Name
stk: State ā†’ Array (Bool Ɨ Entry)
stk
:
Array: Type ?u.1995 ā†’ Type ?u.1995
Array
(
Bool: Type
Bool
Ɨ
Entry: Type
Entry
) deriving
Inhabited: Sort u ā†’ Sort (max1u)
Inhabited
class
OfState: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ (State ā†’ Alloc Ī±) ā†’ ((Alloc Ī± ā†’ Alloc Ī±) ā†’ State ā†’ State) ā†’ OfState Ī±
OfState
(
Ī±: Type
Ī±
:
Type: Type 1
Type
) [
BEq: Type ?u.3631 ā†’ Type ?u.3631
BEq
Ī±: Type
Ī±
] [
Hashable: Sort ?u.3634 ā†’ Sort (max1?u.3634)
Hashable
Ī±: Type
Ī±
] where
get: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [self : OfState Ī±] ā†’ State ā†’ Alloc Ī±
get
:
State: Type
State
ā†’
Alloc: (Ī± : Type ?u.3641) ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type ?u.3641
Alloc
Ī±: Type
Ī±
modify: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [self : OfState Ī±] ā†’ (Alloc Ī± ā†’ Alloc Ī±) ā†’ State ā†’ State
modify
: (
Alloc: (Ī± : Type ?u.3655) ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type ?u.3655
Alloc
Ī±: Type
Ī±
ā†’
Alloc: (Ī± : Type ?u.3659) ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type ?u.3659
Alloc
Ī±: Type
Ī±
) ā†’
State: Type
State
ā†’
State: Type
State
instance: OfState Name
instance
:
OfState: (Ī± : Type) ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type
OfState
Name: Type
Name
where get
s: ?m.3686
s
:=
s: ?m.3686
s
.
names: State ā†’ Alloc Name
names
modify
f: ?m.3694
f
s: ?m.3698
s
:= {
s: ?m.3698
s
with names :=
f: ?m.3694
f
s: ?m.3698
s
.
names: State ā†’ Alloc Name
names
}
instance: OfState Level
instance
:
OfState: (Ī± : Type) ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type
OfState
Level: Type
Level
where get
s: ?m.4006
s
:=
s: ?m.4006
s
.
levels: State ā†’ Alloc Level
levels
modify
f: ?m.4014
f
s: ?m.4018
s
:= {
s: ?m.4018
s
with levels :=
f: ?m.4014
f
s: ?m.4018
s
.
levels: State ā†’ Alloc Level
levels
}
instance: OfState Expr
instance
:
OfState: (Ī± : Type) ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type
OfState
Expr: Type
Expr
where get
s: ?m.4269
s
:=
s: ?m.4269
s
.
exprs: State ā†’ Alloc Expr
exprs
modify
f: ?m.4277
f
s: ?m.4281
s
:= {
s: ?m.4281
s
with exprs :=
f: ?m.4277
f
s: ?m.4281
s
.
exprs: State ā†’ Alloc Expr
exprs
} end Export abbrev
ExportM: Type ā†’ Type
ExportM
:=
StateT: Type ?u.4520 ā†’ (Type ?u.4520 ā†’ Type ?u.4519) ā†’ Type ?u.4520 ā†’ Type (max?u.4520?u.4519)
StateT
Export.State: Type
Export.State
CoreM: Type ā†’ Type
CoreM
namespace Export def
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
{
Ī±: ?m.4530
Ī±
} [
BEq: Type ?u.4533 ā†’ Type ?u.4533
BEq
Ī±: ?m.4530
Ī±
] [
Hashable: Sort ?u.4536 ā†’ Sort (max1?u.4536)
Hashable
Ī±: ?m.4530
Ī±
] [
OfState: (Ī± : Type) ā†’ [inst : BEq Ī±] ā†’ [inst : Hashable Ī±] ā†’ Type
OfState
Ī±: ?m.4530
Ī±
] (
a: Ī±
a
:
Ī±: ?m.4530
Ī±
) :
ExportM: Type ā†’ Type
ExportM
Nat: Type
Nat
:= do let
n: ?m.4702
n
:= (
OfState.get: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [self : OfState Ī±] ā†’ State ā†’ Alloc Ī±
OfState.get
(Ī± :=
Ī±: Type
Ī±
)
(ā† get): ?m.4699
(ā†
get: {Ļƒ : outParam (Type ?u.4630)} ā†’ {m : Type ?u.4630 ā†’ Type ?u.4629} ā†’ [self : MonadState Ļƒ m] ā†’ m Ļƒ
get
(ā† get): ?m.4699
)
).
next: {Ī± : Type ?u.4713} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ Alloc Ī± ā†’ Nat
next
modify: {Ļƒ : Type ?u.4758} ā†’ {m : Type ?u.4758 ā†’ Type ?u.4757} ā†’ [inst : MonadState Ļƒ m] ā†’ (Ļƒ ā†’ Ļƒ) ā†’ m PUnit
modify
$
OfState.modify: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [self : OfState Ī±] ā†’ (Alloc Ī± ā†’ Alloc Ī±) ā†’ State ā†’ State
OfState.modify
(Ī± :=
Ī±: Type
Ī±
) fun
s: ?m.4797
s
ā†¦ {map :=
s: ?m.4797
s
.
map: {Ī± : Type ?u.4805} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ Alloc Ī± ā†’ HashMap Ī± Nat
map
.
insert: {Ī± : Type ?u.4810} ā†’ {Ī² : Type ?u.4809} ā†’ {x : BEq Ī±} ā†’ {x_1 : Hashable Ī±} ā†’ HashMap Ī± Ī² ā†’ Ī± ā†’ Ī² ā†’ HashMap Ī± Ī²
insert
a: Ī±
a
n: ?m.4702
n
, next :=
n: ?m.4702
n
+
1: ?m.4830
1
}
pure: {f : Type ?u.4910 ā†’ Type ?u.4909} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.4910} ā†’ Ī± ā†’ f Ī±
pure
n: ?m.4702
n
def
exportName: Name ā†’ ExportM Nat
exportName
(
n: Name
n
:
Name: Type
Name
) :
ExportM: Type ā†’ Type
ExportM
Nat: Type
Nat
:= do match
(ā† get): ?m.5858
(ā†
get: {Ļƒ : outParam (Type ?u.5789)} ā†’ {m : Type ?u.5789 ā†’ Type ?u.5788} ā†’ [self : MonadState Ļƒ m] ā†’ m Ļƒ
get
(ā† get): ?m.5858
)
.
names: State ā†’ Alloc Name
names
.
map: {Ī± : Type ?u.5860} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ Alloc Ī± ā†’ HashMap Ī± Nat
map
.
find?: {Ī± : Type ?u.5873} ā†’ {Ī² : Type ?u.5872} ā†’ {x : BEq Ī±} ā†’ {x_1 : Hashable Ī±} ā†’ HashMap Ī± Ī² ā†’ Ī± ā†’ Option Ī²
find?
n: Name
n
with |
some: {Ī± : Type ?u.5889} ā†’ Ī± ā†’ Option Ī±
some
i: Nat
i
=>
pure: {f : Type ?u.5905 ā†’ Type ?u.5904} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.5905} ā†’ Ī± ā†’ f Ī±
pure
i: Nat
i
|
none: {Ī± : Type ?u.6006} ā†’ Option Ī±
none
=> match
n: Name
n
with |
.anonymous: Name
.anonymous
=>
pure: {f : Type ?u.6019 ā†’ Type ?u.6018} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.6019} ā†’ Ī± ā†’ f Ī±
pure
0: ?m.6044
0
|
.num: Name ā†’ Nat ā†’ Name
.num
p: Name
p
a: Nat
a
=> let
i: ?m.6151
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
n: Name
n
;
IO.println: {Ī± : Type ?u.6236} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.6151
i
} #NI {ā†
exportName: Name ā†’ ExportM Nat
exportName
p: Name
p
} {
a: Nat
a
}";
pure: {f : Type ?u.6532 ā†’ Type ?u.6531} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.6532} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.6151
i
|
.str: Name ā†’ String ā†’ Name
.str
p: Name
p
s => let
i: ?m.6666
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
n: Name
n
;
IO.println: {Ī± : Type ?u.6751} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.6666
i
} #NS {ā†
exportName: Name ā†’ ExportM Nat
exportName
p: Name
p
} {s}";
pure: {f : Type ?u.6937 ā†’ Type ?u.6936} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.6937} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.6666
i
def
exportLevel: Level ā†’ ExportM Nat
exportLevel
(L :
Level: Type
Level
) :
ExportM: Type ā†’ Type
ExportM
Nat: Type
Nat
:= do match
(ā† get): ?m.12119
(ā†
get: {Ļƒ : outParam (Type ?u.12050)} ā†’ {m : Type ?u.12050 ā†’ Type ?u.12049} ā†’ [self : MonadState Ļƒ m] ā†’ m Ļƒ
get
(ā† get): ?m.12119
)
.
levels: State ā†’ Alloc Level
levels
.
map: {Ī± : Type ?u.12121} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ Alloc Ī± ā†’ HashMap Ī± Nat
map
.
find?: {Ī± : Type ?u.12134} ā†’ {Ī² : Type ?u.12133} ā†’ {x : BEq Ī±} ā†’ {x_1 : Hashable Ī±} ā†’ HashMap Ī± Ī² ā†’ Ī± ā†’ Option Ī²
find?
L with |
some: {Ī± : Type ?u.12007} ā†’ Ī± ā†’ Option Ī±
some
i: Nat
i
=>
pure: {f : Type ?u.12166 ā†’ Type ?u.12165} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.12166} ā†’ Ī± ā†’ f Ī±
pure
i: Nat
i
|
none: {Ī± : Type ?u.12011} ā†’ Option Ī±
none
=> match L with |
.zero: Level
.zero
=>
pure: {f : Type ?u.12280 ā†’ Type ?u.12279} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.12280} ā†’ Ī± ā†’ f Ī±
pure
0: ?m.12305
0
|
.succ: Level ā†’ Level
.succ
l => let
i: ?m.12407
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
L;
IO.println: {Ī± : Type ?u.12492} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.12407
i
} #US {ā†
exportLevel: Level ā†’ ExportM Nat
exportLevel
l}";
pure: {f : Type ?u.12740 ā†’ Type ?u.12739} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.12740} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.12407
i
|
.max: Level ā†’ Level ā†’ Level
.max
lā‚: Level
lā‚
lā‚‚: Level
lā‚‚
=> let
i: ?m.12874
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
L;
IO.println: {Ī± : Type ?u.13006} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.12874
i
} #UM {ā†
exportLevel: Level ā†’ ExportM Nat
exportLevel
lā‚: Level
lā‚
} {ā†
exportLevel: Level ā†’ ExportM Nat
exportLevel
lā‚‚: Level
lā‚‚
}";
pure: {f : Type ?u.13192 ā†’ Type ?u.13191} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.13192} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.12874
i
|
.imax: Level ā†’ Level ā†’ Level
.imax
lā‚: Level
lā‚
lā‚‚: Level
lā‚‚
=> let
i: ?m.13330
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
L;
IO.println: {Ī± : Type ?u.13462} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.13330
i
} #UIM {ā†
exportLevel: Level ā†’ ExportM Nat
exportLevel
lā‚: Level
lā‚
} {ā†
exportLevel: Level ā†’ ExportM Nat
exportLevel
lā‚‚: Level
lā‚‚
}";
pure: {f : Type ?u.13648 ā†’ Type ?u.13647} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.13648} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.13330
i
|
.param: Name ā†’ Level
.param
n: Name
n
=> let
i: ?m.13781
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
L;
IO.println: {Ī± : Type ?u.13866} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.13781
i
} #UP {ā†
exportName: Name ā†’ ExportM Nat
exportName
n: Name
n
}";
pure: {f : Type ?u.14004 ā†’ Type ?u.14003} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.14004} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.13781
i
|
.mvar: LMVarId ā†’ Level
.mvar
_ =>
unreachable!: ?m.14059
unreachable!
def
biStr: BinderInfo ā†’ String
biStr
:
BinderInfo: Type
BinderInfo
ā†’
String: Type
String
|
BinderInfo.default: BinderInfo
BinderInfo.default
=>
"#BD": String
"#BD"
|
BinderInfo.implicit: BinderInfo
BinderInfo.implicit
=>
"#BI": String
"#BI"
|
BinderInfo.strictImplicit: BinderInfo
BinderInfo.strictImplicit
=>
"#BS": String
"#BS"
|
BinderInfo.instImplicit: BinderInfo
BinderInfo.instImplicit
=>
"#BC": String
"#BC"
open ConstantInfo in mutual partial def
exportExpr: Expr ā†’ ExportM Nat
exportExpr
(
E: Expr
E
:
Expr: Type
Expr
) :
ExportM: Type ā†’ Type
ExportM
Nat: Type
Nat
:= do match
(ā† get): ?m.24324
(ā†
get: {Ļƒ : outParam (Type ?u.24255)} ā†’ {m : Type ?u.24255 ā†’ Type ?u.24254} ā†’ [self : MonadState Ļƒ m] ā†’ m Ļƒ
get
(ā† get): ?m.24324
)
.
exprs: State ā†’ Alloc Expr
exprs
.
map: {Ī± : Type ?u.24326} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ Alloc Ī± ā†’ HashMap Ī± Nat
map
.
find?: {Ī± : Type ?u.24339} ā†’ {Ī² : Type ?u.24338} ā†’ {x : BEq Ī±} ā†’ {x_1 : Hashable Ī±} ā†’ HashMap Ī± Ī² ā†’ Ī± ā†’ Option Ī²
find?
E: Expr
E
with |
some: {Ī± : Type ?u.24355} ā†’ Ī± ā†’ Option Ī±
some
i: Nat
i
=>
pure: {f : Type ?u.24371 ā†’ Type ?u.24370} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.24371} ā†’ Ī± ā†’ f Ī±
pure
i: Nat
i
|
none: {Ī± : Type ?u.24472} ā†’ Option Ī±
none
=> match
E: Expr
E
with |
.bvar: Nat ā†’ Expr
.bvar
n: Nat
n
=> let
i: ?m.24570
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
E: Expr
E
;
IO.println: {Ī± : Type ?u.24608} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.24570
i
} #EV {
n: Nat
n
}";
pure: {f : Type ?u.24856 ā†’ Type ?u.24855} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.24856} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.24570
i
|
.fvar: FVarId ā†’ Expr
.fvar
_ =>
unreachable!: ?m.24907
unreachable!
|
.mvar: MVarId ā†’ Expr
.mvar
_ =>
unreachable!: ?m.25035
unreachable!
|
.sort: Level ā†’ Expr
.sort
l => let
i: ?m.25211
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
E: Expr
E
;
IO.println: {Ī± : Type ?u.25296} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.25211
i
} #ES {ā†
exportLevel: Level ā†’ ExportM Nat
exportLevel
l}";
pure: {f : Type ?u.25434 ā†’ Type ?u.25433} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.25434} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.25211
i
|
.const: Name ā†’ List Level ā†’ Expr
.const
n: Name
n
ls =>
exportDef: Name ā†’ ExportM Unit
exportDef
n: Name
n
let
i: ?m.25613
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
E: Expr
E
let mut
s: ?m.25663
s
:= s!"{
i: ?m.25613
i
} #EC {ā†
exportName: Name ā†’ ExportM Nat
exportName
n: Name
n
}" for
l: ?m.25855
l
in ls do
s: ?m.25861
s
:=
s: ?m.25861
s
++
s!" {ā† exportLevel l}": ?m.25954
s!
s!" {ā† exportLevel l}": ?m.25954
" {ā†
exportLevel: Level ā†’ ExportM Nat
exportLevel
s!" {ā† exportLevel l}": ?m.25954
l: ?m.25855
l
s!" {ā† exportLevel l}": ?m.25954
}"
IO.println: {Ī± : Type ?u.26217} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s: ?m.26179
s
;
pure: {f : Type ?u.26255 ā†’ Type ?u.26254} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.26255} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.25613
i
|
.app: Expr ā†’ Expr ā†’ Expr
.app
eā‚: Expr
eā‚
eā‚‚: Expr
eā‚‚
=> let
i: ?m.26403
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
E: Expr
E
;
IO.println: {Ī± : Type ?u.26535} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.26403
i
} #EA {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
eā‚: Expr
eā‚
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
eā‚‚: Expr
eā‚‚
}";
pure: {f : Type ?u.26721 ā†’ Type ?u.26720} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.26721} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.26403
i
|
.lam: Name ā†’ Expr ā†’ Expr ā†’ BinderInfo ā†’ Expr
.lam
_
eā‚: Expr
eā‚
eā‚‚: Expr
eā‚‚
d => let
i: ?m.26868
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
E: Expr
E
IO.println: {Ī± : Type ?u.27000} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.26868
i
} #EL {
biStr: BinderInfo ā†’ String
biStr
d} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
eā‚: Expr
eā‚
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
eā‚‚: Expr
eā‚‚
}";
pure: {f : Type ?u.27234 ā†’ Type ?u.27233} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.27234} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.26868
i
|
.forallE: Name ā†’ Expr ā†’ Expr ā†’ BinderInfo ā†’ Expr
.forallE
_
eā‚: Expr
eā‚
eā‚‚: Expr
eā‚‚
d => let
i: ?m.27381
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
E: Expr
E
IO.println: {Ī± : Type ?u.27513} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.27381
i
} #EP {
biStr: BinderInfo ā†’ String
biStr
d} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
eā‚: Expr
eā‚
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
eā‚‚: Expr
eā‚‚
}";
pure: {f : Type ?u.27747 ā†’ Type ?u.27746} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.27747} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.27381
i
|
.letE: Name ā†’ Expr ā†’ Expr ā†’ Expr ā†’ Bool ā†’ Expr
.letE
_
eā‚: Expr
eā‚
eā‚‚: Expr
eā‚‚
eā‚ƒ: Expr
eā‚ƒ
_ => let
i: ?m.27902
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
E: Expr
E
IO.println: {Ī± : Type ?u.28081} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.27902
i
} #EP {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
eā‚: Expr
eā‚
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
eā‚‚: Expr
eā‚‚
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
eā‚ƒ: Expr
eā‚ƒ
}";
pure: {f : Type ?u.28315 ā†’ Type ?u.28314} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.28315} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.27902
i
|
.lit: Literal ā†’ Expr
.lit
(
.natVal: Nat ā†’ Literal
.natVal
n: Nat
n
) => let
i: ?m.28454
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
E: Expr
E
;
IO.println: {Ī± : Type ?u.28492} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.28454
i
} #EN {
n: Nat
n
}";
pure: {f : Type ?u.28630 ā†’ Type ?u.28629} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.28630} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.28454
i
|
.lit: Literal ā†’ Expr
.lit
(
.strVal: String ā†’ Literal
.strVal
s) => let
i: ?m.28751
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
E: Expr
E
;
IO.println: {Ī± : Type ?u.28789} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.28751
i
} #ET {s}";
pure: {f : Type ?u.28927 ā†’ Type ?u.28926} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.28927} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.28751
i
|
.mdata: MData ā†’ Expr ā†’ Expr
.mdata
_ _ =>
unreachable!: ?m.28981
unreachable!
|
.proj: Name ā†’ Nat ā†’ Expr ā†’ Expr
.proj
n: Name
n
k: Nat
k
e: Expr
e
=> let
i: ?m.29167
i
ā†
alloc: {Ī± : Type} ā†’ [inst : BEq Ī±] ā†’ [inst_1 : Hashable Ī±] ā†’ [inst : OfState Ī±] ā†’ Ī± ā†’ ExportM Nat
alloc
E: Expr
E
;
IO.println: {Ī± : Type ?u.29299} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s!"{
i: ?m.29167
i
} #EJ {ā†
exportName: Name ā†’ ExportM Nat
exportName
n: Name
n
} {
k: Nat
k
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
e: Expr
e
}";
pure: {f : Type ?u.29533 ā†’ Type ?u.29532} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.29533} ā†’ Ī± ā†’ f Ī±
pure
i: ?m.29167
i
partial def
exportDef: Name ā†’ ExportM Unit
exportDef
(
n: Name
n
:
Name: Type
Name
) :
ExportM: Type ā†’ Type
ExportM
Unit: Type
Unit
:= do if
(ā† get): ?m.36613
(ā†
get: {Ļƒ : outParam (Type ?u.36545)} ā†’ {m : Type ?u.36545 ā†’ Type ?u.36544} ā†’ [self : MonadState Ļƒ m] ā†’ m Ļƒ
get
(ā† get): ?m.36613
)
.
defs: State ā†’ HashSet Name
defs
.
contains: {Ī± : Type ?u.36624} ā†’ {x : BEq Ī±} ā†’ {x_1 : Hashable Ī±} ā†’ HashSet Ī± ā†’ Ī± ā†’ Bool
contains
n: Name
n
then
return: ?m.36730 ?m.36732
return
let
ci: ?m.36938
ci
ā†
getConstInfo: {m : Type ā†’ Type} ā†’ [inst : Monad m] ā†’ [inst : MonadEnv m] ā†’ [inst : MonadError m] ā†’ Name ā†’ m ConstantInfo
getConstInfo
n: Name
n
for
c: ?m.37025
c
in
ci: ?m.36938
ci
.
value!: ConstantInfo ā†’ Expr
value!
.
getUsedConstants: Expr ā†’ Array Name
getUsedConstants
do unless
(ā† get): ?m.37120
(ā†
get: {Ļƒ : outParam (Type ?u.37067)} ā†’ {m : Type ?u.37067 ā†’ Type ?u.37066} ā†’ [self : MonadState Ļƒ m] ā†’ m Ļƒ
get
(ā† get): ?m.37120
)
.
defs: State ā†’ HashSet Name
defs
.
contains: {Ī± : Type ?u.37122} ā†’ {x : BEq Ī±} ā†’ {x_1 : Hashable Ī±} ā†’ HashSet Ī± ā†’ Ī± ā†’ Bool
contains
c: ?m.37025
c
do
exportDef: Name ā†’ ExportM Unit
exportDef
c: ?m.37025
c
match
ci: ?m.36938
ci
with |
axiomInfo: AxiomVal ā†’ ConstantInfo
axiomInfo
val =>
axdef: String ā†’ Name ā†’ Expr ā†’ List Name ā†’ ExportM Unit
axdef
"#AX": String
"#AX"
val.
name: ConstantVal ā†’ Name
name
val.
type: ConstantVal ā†’ Expr
type
val.
levelParams: ConstantVal ā†’ List Name
levelParams
|
defnInfo: DefinitionVal ā†’ ConstantInfo
defnInfo
val =>
defn: String ā†’ Name ā†’ Expr ā†’ Expr ā†’ List Name ā†’ ExportM Unit
defn
"#DEF": String
"#DEF"
val.
name: ConstantVal ā†’ Name
name
val.
type: ConstantVal ā†’ Expr
type
val.
value: DefinitionVal ā†’ Expr
value
val.
levelParams: ConstantVal ā†’ List Name
levelParams
|
thmInfo: TheoremVal ā†’ ConstantInfo
thmInfo
val =>
defn: String ā†’ Name ā†’ Expr ā†’ Expr ā†’ List Name ā†’ ExportM Unit
defn
"#THM": String
"#THM"
val.
name: ConstantVal ā†’ Name
name
val.
type: ConstantVal ā†’ Expr
type
val.
value: TheoremVal ā†’ Expr
value
val.
levelParams: ConstantVal ā†’ List Name
levelParams
|
opaqueInfo: OpaqueVal ā†’ ConstantInfo
opaqueInfo
val =>
defn: String ā†’ Name ā†’ Expr ā†’ Expr ā†’ List Name ā†’ ExportM Unit
defn
"#CN": String
"#CN"
val.
name: ConstantVal ā†’ Name
name
val.
type: ConstantVal ā†’ Expr
type
val.
value: OpaqueVal ā†’ Expr
value
val.
levelParams: ConstantVal ā†’ List Name
levelParams
|
quotInfo: QuotVal ā†’ ConstantInfo
quotInfo
_ =>
IO.println: {Ī± : Type ?u.37536} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
"#QUOT": String
"#QUOT"
for
n: ?m.37751
n
in [``
Quot: {Ī± : Sort u} ā†’ (Ī± ā†’ Ī± ā†’ Prop) ā†’ Sort u
Quot
, ``
Quot.mk: {Ī± : Sort u} ā†’ (r : Ī± ā†’ Ī± ā†’ Prop) ā†’ Ī± ā†’ Quot r
Quot.mk
, ``
Quot.lift: {Ī± : Sort u} ā†’ {r : Ī± ā†’ Ī± ā†’ Prop} ā†’ {Ī² : Sort v} ā†’ (f : Ī± ā†’ Ī²) ā†’ (āˆ€ (a b : Ī±), r a b ā†’ f a = f b) ā†’ Quot r ā†’ Ī²
Quot.lift
, ``
Quot.ind: āˆ€ {Ī± : Sort u} {r : Ī± ā†’ Ī± ā†’ Prop} {Ī² : Quot r ā†’ Prop}, (āˆ€ (a : Ī±), Ī² (Quot.mk r a)) ā†’ āˆ€ (q : Quot r), Ī² q
Quot.ind
] do
insert: Name ā†’ ExportM Unit
insert
n: ?m.37751
n
|
inductInfo: InductiveVal ā†’ ConstantInfo
inductInfo
val =>
ind: List Name ā†’ ExportM Unit
ind
val.
all: InductiveVal ā†’ List Name
all
|
ctorInfo: ConstructorVal ā†’ ConstantInfo
ctorInfo
val =>
ind: List Name ā†’ ExportM Unit
ind
(ā† getConstInfoInduct val.induct): ?m.38027
(ā†
getConstInfoInduct: {m : Type ā†’ Type} ā†’ [inst : Monad m] ā†’ [inst : MonadEnv m] ā†’ [inst : MonadError m] ā†’ Name ā†’ m InductiveVal
getConstInfoInduct
(ā† getConstInfoInduct val.induct): ?m.38027
val
(ā† getConstInfoInduct val.induct): ?m.38027
.
induct: ConstructorVal ā†’ Name
induct
(ā† getConstInfoInduct val.induct): ?m.38027
)
.
all: InductiveVal ā†’ List Name
all
|
recInfo: RecursorVal ā†’ ConstantInfo
recInfo
val =>
ind: List Name ā†’ ExportM Unit
ind
val.
all: RecursorVal ā†’ List Name
all
where
insert: Name ā†’ ExportM Unit
insert
(
n: Name
n
:
Name: Type
Name
) :
ExportM: Type ā†’ Type
ExportM
Unit: Type
Unit
:=
modify: {Ļƒ : Type ?u.30156} ā†’ {m : Type ?u.30156 ā†’ Type ?u.30155} ā†’ [inst : MonadState Ļƒ m] ā†’ (Ļƒ ā†’ Ļƒ) ā†’ m PUnit
modify
fun
s: ?m.30190
s
ā†¦ {
s: ?m.30190
s
with defs :=
s: ?m.30190
s
.
defs: State ā†’ HashSet Name
defs
.
insert: {Ī± : Type ?u.30472} ā†’ {x : BEq Ī±} ā†’ {x_1 : Hashable Ī±} ā†’ HashSet Ī± ā†’ Ī± ā†’ HashSet Ī±
insert
n: Name
n
}
defn: String ā†’ Name ā†’ Expr ā†’ Expr ā†’ List Name ā†’ ExportM Unit
defn
(
ty: String
ty
:
String: Type
String
) (
n: Name
n
:
Name: Type
Name
) (
t: Expr
t
e: Expr
e
:
Expr: Type
Expr
) (ls :
List: Type ?u.30110 ā†’ Type ?u.30110
List
Name: Type
Name
) :
ExportM: Type ā†’ Type
ExportM
Unit: Type
Unit
:= do let mut
s: ?m.30741
s
:= s!"{
ty: String
ty
} {ā†
exportName: Name ā†’ ExportM Nat
exportName
n: Name
n
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
t: Expr
t
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
e: Expr
e
}" for
l: ?m.30735
l
in ls do
s: ?m.30791
s
:=
s: ?m.30741
s
++
s!" {ā† exportName l}": ?m.30834
s!
s!" {ā† exportName l}": ?m.30834
" {ā†
exportName: Name ā†’ ExportM Nat
exportName
s!" {ā† exportName l}": ?m.30834
l: ?m.30735
l
s!" {ā† exportName l}": ?m.30834
}"
IO.println: {Ī± : Type ?u.31119} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s: ?m.31081
s
insert: Name ā†’ ExportM Unit
insert
n: Name
n
axdef: String ā†’ Name ā†’ Expr ā†’ List Name ā†’ ExportM Unit
axdef
(
ty: String
ty
:
String: Type
String
) (
n: Name
n
:
Name: Type
Name
) (
t: Expr
t
:
Expr: Type
Expr
) (ls :
List: Type ?u.30121 ā†’ Type ?u.30121
List
Name: Type
Name
) :
ExportM: Type ā†’ Type
ExportM
Unit: Type
Unit
:= do let mut
s: ?m.31624
s
:= s!"{
ty: String
ty
} {ā†
exportName: Name ā†’ ExportM Nat
exportName
n: Name
n
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
t: Expr
t
}" for
l: ?m.31618
l
in ls do
s: ?m.31674
s
:=
s: ?m.31624
s
++
s!" {ā† exportName l}": ?m.31717
s!
s!" {ā† exportName l}": ?m.31717
" {ā†
exportName: Name ā†’ ExportM Nat
exportName
s!" {ā† exportName l}": ?m.31717
l: ?m.31618
l
s!" {ā† exportName l}": ?m.31717
}"
IO.println: {Ī± : Type ?u.31913} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s: ?m.31875
s
insert: Name ā†’ ExportM Unit
insert
n: Name
n
ind: List Name ā†’ ExportM Unit
ind
:
List: Type ?u.30127 ā†’ Type ?u.30127
List
Name: Type
Name
ā†’
ExportM: Type ā†’ Type
ExportM
Unit: Type
Unit
| [] =>
unreachable!: ?m.31999
unreachable!
| is@(
i: Name
i
::_) => do let
val: ?m.32437
val
ā†
getConstInfoInduct: {m : Type ā†’ Type} ā†’ [inst : Monad m] ā†’ [inst : MonadEnv m] ā†’ [inst : MonadError m] ā†’ Name ā†’ m InductiveVal
getConstInfoInduct
i: Name
i
let mut
s: ?m.32440
s
:= match is.
length: {Ī± : Type ?u.33495} ā†’ List Ī± ā†’ Nat
length
with |
1: Nat
1
=> s!"#IND {
val: ?m.32437
val
.
numParams: InductiveVal ā†’ Nat
numParams
}" |
n: Nat
n
=> s!"#MUT {
val: ?m.32437
val
.
numParams: InductiveVal ā†’ Nat
numParams
} {
n: Nat
n
}" for
j: ?m.32522
j
in is do
insert: Name ā†’ ExportM Unit
insert
j: ?m.32522
j
;
insert: Name ā†’ ExportM Unit
insert
(
mkRecName: Name ā†’ Name
mkRecName
j: ?m.32522
j
) for
j: ?m.32763
j
in is do let
val: ?m.32863
val
ā†
getConstInfoInduct: {m : Type ā†’ Type} ā†’ [inst : Monad m] ā†’ [inst : MonadEnv m] ā†’ [inst : MonadError m] ā†’ Name ā†’ m InductiveVal
getConstInfoInduct
j: ?m.32763
j
s: ?m.34106
s
:=
s: ?m.32769
s
++ s!" {ā†
exportName: Name ā†’ ExportM Nat
exportName
val: ?m.32863
val
.
name: ConstantVal ā†’ Name
name
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
val: ?m.32863
val
.
type: ConstantVal ā†’ Expr
type
} {
val: ?m.32863
val
.
ctors: InductiveVal ā†’ List Name
ctors
.
length: {Ī± : Type ?u.33001} ā†’ List Ī± ā†’ Nat
length
}" for
c: ?m.33215
c
in
val: ?m.32863
val
.
ctors: InductiveVal ā†’ List Name
ctors
do
insert: Name ā†’ ExportM Unit
insert
c: ?m.33215
c
s: ?m.33221
s
:=
s: ?m.33221
s
++
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.33825
s!
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.33825
" {ā†
exportName: Name ā†’ ExportM Nat
exportName
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.33825
c: ?m.33215
c
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.33825
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.33825
(ā† getConstInfoCtor c): ?m.33409
(ā†
getConstInfoCtor: {m : Type ā†’ Type} ā†’ [inst : Monad m] ā†’ [inst : MonadEnv m] ā†’ [inst : MonadError m] ā†’ Name ā†’ m ConstructorVal
getConstInfoCtor
(ā† getConstInfoCtor c): ?m.33409
c: ?m.33215
c
(ā† getConstInfoCtor c): ?m.33409
)
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.33825
.
type: ConstantVal ā†’ Expr
type
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.33825
}"
for
j: ?m.34346
j
in is do
s: ?m.34403
s
ā†
indbody: Name ā†’ String ā†’ ExportM String
indbody
j: ?m.34346
j
s: ?m.34352
s
for
l: ?m.34613
l
in
val: ?m.32437
val
.
levelParams: ConstantVal ā†’ List Name
levelParams
do
s: ?m.34669
s
:=
s: ?m.34619
s
++
s!" {ā† exportName l}": ?m.34715
s!
s!" {ā† exportName l}": ?m.34715
" {ā†
exportName: Name ā†’ ExportM Nat
exportName
s!" {ā† exportName l}": ?m.34715
l: ?m.34613
l
s!" {ā† exportName l}": ?m.34715
}"
IO.println: {Ī± : Type ?u.34876} ā†’ [inst : ToString Ī±] ā†’ Ī± ā†’ IO Unit
IO.println
s: ?m.34874
s
indbody: Name ā†’ String ā†’ ExportM String
indbody
(
ind: Name
ind
:
Name: Type
Name
) (s :
String: Type
String
) :
ExportM: Type ā†’ Type
ExportM
String: Type
String
:= do let
val: ?m.35458
val
ā†
getConstInfoInduct: {m : Type ā†’ Type} ā†’ [inst : Monad m] ā†’ [inst : MonadEnv m] ā†’ [inst : MonadError m] ā†’ Name ā†’ m InductiveVal
getConstInfoInduct
ind: Name
ind
let mut
s: ?m.35555
s
:= s ++ s!" {ā†
exportName: Name ā†’ ExportM Nat
exportName
ind: Name
ind
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
val: ?m.35458
val
.
type: ConstantVal ā†’ Expr
type
} {
val: ?m.35458
val
.
ctors: InductiveVal ā†’ List Name
ctors
.
length: {Ī± : Type ?u.35599} ā†’ List Ī± ā†’ Nat
length
}" for
c: ?m.35844
c
in
val: ?m.35458
val
.
ctors: InductiveVal ā†’ List Name
ctors
do
s: ?m.35850
s
:=
s: ?m.35850
s
++
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.36132
s!
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.36132
" {ā†
exportName: Name ā†’ ExportM Nat
exportName
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.36132
c: ?m.35844
c
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.36132
} {ā†
exportExpr: Expr ā†’ ExportM Nat
exportExpr
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.36132
(ā† getConstInfoCtor c): ?m.35991
(ā†
getConstInfoCtor: {m : Type ā†’ Type} ā†’ [inst : Monad m] ā†’ [inst : MonadEnv m] ā†’ [inst : MonadError m] ā†’ Name ā†’ m ConstructorVal
getConstInfoCtor
(ā† getConstInfoCtor c): ?m.35991
c: ?m.35844
c
(ā† getConstInfoCtor c): ?m.35991
)
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.36132
.
type: ConstantVal ā†’ Expr
type
s!" {ā† exportName c} {ā† exportExpr (ā† getConstInfoCtor c).type}": ?m.36132
}"
pure: {f : Type ?u.36387 ā†’ Type ?u.36386} ā†’ [self : Pure f] ā†’ {Ī± : Type ?u.36387} ā†’ Ī± ā†’ f Ī±
pure
s: ?m.36384
s
end def
runExportM: {Ī± : Type} ā†’ ExportM Ī± ā†’ CoreM Ī±
runExportM
(
m: ExportM Ī±
m
:
ExportM: Type ā†’ Type
ExportM
Ī±: ?m.95311
Ī±
) :
CoreM: Type ā†’ Type
CoreM
Ī±: ?m.95311
Ī±
:=
m: ExportM Ī±
m
.
run': {Ļƒ : Type ?u.95322} ā†’ {m : Type ?u.95322 ā†’ Type ?u.95321} ā†’ [inst : Functor m] ā†’ {Ī± : Type ?u.95322} ā†’ StateT Ļƒ m Ī± ā†’ Ļƒ ā†’ m Ī±
run'
default: {Ī± : Sort ?u.95371} ā†’ [self : Inhabited Ī±] ā†’ Ī±
default
-- #eval runExportM (exportDef `Lean.Expr) end Export end Lean